coq 8.7.2 · OCaml Package

type evar = Term.existential_key

val string_of_existential : evar -> string

module Filter : sig ... end

type evar_body =

| Evar_empty
| Evar_defined of Term.constr

module Store : Store.S

type evar_info = {

evar_concl : Term.constr;
evar_hyps : Environ.named_context_val;
evar_body : evar_body;
evar_filter : Filter.t;
evar_source : Evar_kinds.t Loc.located;
evar_candidates : Term.constr list option;
evar_extra : Store.t;

}

val make_evar : Environ.named_context_val -> Term.types -> evar_info

val evar_concl : evar_info -> Term.constr

val evar_context : evar_info -> Context.Named.t

val evar_filtered_context : evar_info -> Context.Named.t

val evar_hyps : evar_info -> Environ.named_context_val

val evar_filtered_hyps : evar_info -> Environ.named_context_val

val evar_body : evar_info -> evar_body

val evar_filter : evar_info -> Filter.t

val evar_env : evar_info -> Environ.env

val evar_filtered_env : evar_info -> Environ.env

val map_evar_body : (Term.constr -> Term.constr) -> evar_body -> evar_body

val map_evar_info : (Term.constr -> Term.constr) -> evar_info -> evar_info

type evar_universe_context = UState.t

type evar_map

val empty : evar_map

val from_env : Environ.env -> evar_map

val from_ctx : evar_universe_context -> evar_map

val is_empty : evar_map -> bool

val has_undefined : evar_map -> bool

val new_evar : evar_map -> ?name:Names.Id.t -> evar_info -> evar_map * evar

val add : evar_map -> evar -> evar_info -> evar_map

val find : evar_map -> evar -> evar_info

val find_undefined : evar_map -> evar -> evar_info

val remove : evar_map -> evar -> evar_map

val mem : evar_map -> evar -> bool

val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

val fold_undefined : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

val raw_map : (evar -> evar_info -> evar_info) -> evar_map -> evar_map

val raw_map_undefined : 
  (evar -> evar_info -> evar_info) ->
  evar_map ->
  evar_map

val define : evar -> Term.constr -> evar_map -> evar_map

val cmap : (Term.constr -> Term.constr) -> evar_map -> evar_map

val is_evar : evar_map -> evar -> bool

val is_defined : evar_map -> evar -> bool

val is_undefined : evar_map -> evar -> bool

val add_constraints : evar_map -> Univ.constraints -> evar_map

val undefined_map : evar_map -> evar_info Evar.Map.t

val drop_all_defined : evar_map -> evar_map

exception NotInstantiatedEvar

val existential_value : evar_map -> Term.existential -> Term.constr

val existential_type : evar_map -> Term.existential -> Term.types

val existential_opt_value : evar_map -> Term.existential -> Term.constr option

val evar_instance_array : 
  (Context.Named.Declaration.t -> 'a -> bool) ->
  evar_info ->
  'a array ->
  (Names.Id.t * 'a) list

val instantiate_evar_array : 
  evar_info ->
  Term.constr ->
  Term.constr array ->
  Term.constr

val evars_reset_evd : 
  ?with_conv_pbs:bool ->
  ?with_univs:bool ->
  evar_map ->
  evar_map ->
  evar_map

val restrict : 
  evar ->
  Filter.t ->
  ?candidates:Term.constr list ->
  ?src:Evar_kinds.t Loc.located ->
  evar_map ->
  evar_map * evar

val is_restricted_evar : evar_info -> evar option

val downcast : evar -> Term.types -> evar_map -> evar_map

val evar_source : Term.existential_key -> evar_map -> Evar_kinds.t Loc.located

val evar_ident : Term.existential_key -> evar_map -> Names.Id.t option

val rename : Term.existential_key -> Names.Id.t -> evar_map -> evar_map

val evar_key : Names.Id.t -> evar_map -> Term.existential_key

val evar_source_of_meta : 
  Term.metavariable ->
  evar_map ->
  Evar_kinds.t Loc.located

val dependent_evar_ident : Term.existential_key -> evar_map -> Names.Id.t

val emit_side_effects : Safe_typing.private_constants -> evar_map -> evar_map

val eval_side_effects : evar_map -> Safe_typing.private_constants

val drop_side_effects : evar_map -> evar_map

val declare_future_goal : Evar.t -> evar_map -> evar_map

val declare_principal_goal : Evar.t -> evar_map -> evar_map

val future_goals : evar_map -> Evar.t list

val principal_future_goal : evar_map -> Evar.t option

val reset_future_goals : evar_map -> evar_map

val restore_future_goals : evar_map -> Evar.t list -> Evar.t option -> evar_map

val whd_sort_variable : evar_map -> Term.constr -> Term.constr

exception UniversesDiffer

val add_universe_constraints : 
  evar_map ->
  Universes.universe_constraints ->
  evar_map

val get_extra_data : evar_map -> Store.t

val set_extra_data : Store.t -> evar_map -> evar_map

type !'a sigma = {

it : 'a;
sigma : evar_map;

}

val sig_it : 'a sigma -> 'a

val sig_sig : 'a sigma -> evar_map

val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b

module MonadR : sig ... end

module Monad : sig ... end

module Metaset : sig ... end

module Metamap : sig ... end

type !'a freelisted = {

rebus : 'a;
freemetas : Metaset.t;

}

val metavars_of : Term.constr -> Metaset.t

val mk_freelisted : Term.constr -> Term.constr freelisted

val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted

type instance_constraint =

| IsSuperType
| IsSubType
| Conv

val eq_instance_constraint : instance_constraint -> instance_constraint -> bool

type instance_typing_status =

| CoerceToType
| TypeNotProcessed
| TypeProcessed

type instance_status = instance_constraint * instance_typing_status

type clbinding =

| Cltyp of Names.Name.t * Term.constr freelisted
| Clval of Names.Name.t * Term.constr freelisted * instance_status * Term.constr freelisted

type conv_pb = Reduction.conv_pb

type evar_constraint = conv_pb * Environ.env * Term.constr * Term.constr

val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map

val extract_changed_conv_pbs : 
  evar_map ->
  (Evar.Set.t -> evar_constraint -> bool) ->
  evar_map * evar_constraint list

val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list

val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t option

val evars_of_term : Term.constr -> Evar.Set.t

val evars_of_named_context : Context.Named.t -> Evar.Set.t

val evars_of_filtered_evar_info : evar_info -> Evar.Set.t

val meta_list : evar_map -> (Term.metavariable * clbinding) list

val meta_defined : evar_map -> Term.metavariable -> bool

val meta_value : evar_map -> Term.metavariable -> Term.constr

val meta_fvalue : 
  evar_map ->
  Term.metavariable ->
  Term.constr freelisted * instance_status

val meta_opt_fvalue : 
  evar_map ->
  Term.metavariable ->
  (Term.constr freelisted * instance_status) option

val meta_type : evar_map -> Term.metavariable -> Term.types

val meta_ftype : evar_map -> Term.metavariable -> Term.types freelisted

val meta_name : evar_map -> Term.metavariable -> Names.Name.t

val meta_declare : 
  Term.metavariable ->
  Term.types ->
  ?name:Names.Name.t ->
  evar_map ->
  evar_map

val meta_assign : 
  Term.metavariable ->
  (Term.constr * instance_status) ->
  evar_map ->
  evar_map

val meta_reassign : 
  Term.metavariable ->
  (Term.constr * instance_status) ->
  evar_map ->
  evar_map

val clear_metas : evar_map -> evar_map

val meta_merge : ?with_univs:bool -> evar_map -> evar_map -> evar_map

val undefined_metas : evar_map -> Term.metavariable list

val map_metas_fvalue : (Term.constr -> Term.constr) -> evar_map -> evar_map

val map_metas : (Term.constr -> Term.constr) -> evar_map -> evar_map

type metabinding = Term.metavariable * Term.constr * instance_status

val retract_coercible_metas : evar_map -> metabinding list * evar_map

type rigid = UState.rigid =

| UnivRigid
| UnivFlexible of bool

val univ_rigid : rigid

val univ_flexible : rigid

val univ_flexible_alg : rigid

type !'a in_evar_universe_context = 'a * evar_universe_context

val evar_universe_context_set : 
  evar_universe_context ->
  Univ.universe_context_set

val evar_universe_context_constraints : 
  evar_universe_context ->
  Univ.constraints

val evar_context_universe_context : 
  evar_universe_context ->
  Univ.universe_context

val evar_universe_context_of : 
  Univ.universe_context_set ->
  evar_universe_context

val empty_evar_universe_context : evar_universe_context

val union_evar_universe_context : 
  evar_universe_context ->
  evar_universe_context ->
  evar_universe_context

val evar_universe_context_subst : 
  evar_universe_context ->
  Universes.universe_opt_subst

val constrain_variables : 
  Univ.LSet.t ->
  evar_universe_context ->
  Univ.constraints

val evar_universe_context_of_binders : 
  Universes.universe_binders ->
  evar_universe_context

val make_evar_universe_context : 
  Environ.env ->
  Names.Id.t Loc.located list option ->
  evar_universe_context

val restrict_universe_context : evar_map -> Univ.universe_set -> evar_map

val universe_of_name : evar_map -> string -> Univ.universe_level

val add_universe_name : evar_map -> string -> Univ.universe_level -> evar_map

val add_constraints_context : 
  evar_universe_context ->
  Univ.constraints ->
  evar_universe_context

val normalize_evar_universe_context_variables : 
  evar_universe_context ->
  Univ.universe_subst in_evar_universe_context

val normalize_evar_universe_context : 
  evar_universe_context ->
  evar_universe_context

val new_univ_level_variable : 
  ?loc:Loc.t ->
  ?name:string ->
  rigid ->
  evar_map ->
  evar_map * Univ.universe_level

val new_univ_variable : 
  ?loc:Loc.t ->
  ?name:string ->
  rigid ->
  evar_map ->
  evar_map * Univ.universe

val new_sort_variable : 
  ?loc:Loc.t ->
  ?name:string ->
  rigid ->
  evar_map ->
  evar_map * Term.sorts

val add_global_univ : evar_map -> Univ.Level.t -> evar_map

val universe_rigidity : evar_map -> Univ.Level.t -> rigid

val make_flexible_variable : 
  evar_map ->
  algebraic:bool ->
  Univ.universe_level ->
  evar_map

val is_sort_variable : evar_map -> Term.sorts -> Univ.universe_level option

val is_flexible_level : evar_map -> Univ.Level.t -> bool

val normalize_universe : evar_map -> Univ.universe -> Univ.universe

val normalize_universe_instance : 
  evar_map ->
  Univ.universe_instance ->
  Univ.universe_instance

val set_leq_sort : 
  Environ.env ->
  evar_map ->
  Term.sorts ->
  Term.sorts ->
  evar_map

val set_eq_sort : 
  Environ.env ->
  evar_map ->
  Term.sorts ->
  Term.sorts ->
  evar_map

val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map

val set_eq_level : 
  evar_map ->
  Univ.universe_level ->
  Univ.universe_level ->
  evar_map

val set_leq_level : 
  evar_map ->
  Univ.universe_level ->
  Univ.universe_level ->
  evar_map

val set_eq_instances : 
  ?flex:bool ->
  evar_map ->
  Univ.universe_instance ->
  Univ.universe_instance ->
  evar_map

val check_eq : evar_map -> Univ.universe -> Univ.universe -> bool

val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool

val evar_universe_context : evar_map -> evar_universe_context

val universe_context_set : evar_map -> Univ.universe_context_set

val universe_context : 
  ?names:Names.Id.t Loc.located list ->
  evar_map ->
  (Names.Id.t * Univ.Level.t) list * Univ.universe_context

val universe_subst : evar_map -> Universes.universe_opt_subst

val universes : evar_map -> UGraph.t

val merge_universe_context : evar_map -> evar_universe_context -> evar_map

val set_universe_context : evar_map -> evar_universe_context -> evar_map

val merge_context_set : 
  ?loc:Loc.t ->
  ?sideff:bool ->
  rigid ->
  evar_map ->
  Univ.universe_context_set ->
  evar_map

val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map

val with_context_set : 
  ?loc:Loc.t ->
  rigid ->
  evar_map ->
  'a Univ.in_universe_context_set ->
  evar_map * 'a

val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst

val abstract_undefined_variables : 
  evar_universe_context ->
  evar_universe_context

val fix_undefined_variables : evar_map -> evar_map

val refresh_undefined_universes : 
  evar_map ->
  evar_map * Univ.universe_level_subst

val nf_constraints : evar_map -> evar_map

val update_sigma_env : evar_map -> Environ.env -> evar_map

val fresh_sort_in_family : 
  ?loc:Loc.t ->
  ?rigid:rigid ->
  Environ.env ->
  evar_map ->
  Term.sorts_family ->
  evar_map * Term.sorts

val fresh_constant_instance : 
  ?loc:Loc.t ->
  Environ.env ->
  evar_map ->
  Names.constant ->
  evar_map * Term.pconstant

val fresh_inductive_instance : 
  ?loc:Loc.t ->
  Environ.env ->
  evar_map ->
  Names.inductive ->
  evar_map * Term.pinductive

val fresh_constructor_instance : 
  ?loc:Loc.t ->
  Environ.env ->
  evar_map ->
  Names.constructor ->
  evar_map * Term.pconstructor

val fresh_global : 
  ?loc:Loc.t ->
  ?rigid:rigid ->
  ?names:Univ.Instance.t ->
  Environ.env ->
  evar_map ->
  Globnames.global_reference ->
  evar_map * Term.constr

type open_constr = evar_map * Term.constr

type unsolvability_explanation =

| SeveralInstancesFound of int

val create_evar_defs : evar_map -> evar_map

val evar_counter_summary_name : string

package coq