coq 8.8.1 · OCaml Package

type evar = Evar.t

deprecated use Evar.t

val string_of_existential : Evar.t -> string

deprecated use Evar.print

module Filter : sig ... end

type evar_body =

| Evar_empty
| Evar_defined of Constr.constr

module Store : Store.S

type evar_info = {

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

}

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

val evar_concl : evar_info -> Constr.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 : (Constr.constr -> Constr.constr) -> evar_body -> evar_body

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

type evar_universe_context = UState.t

deprecated Alias of UState.t

type evar_map

val empty : evar_map

val from_env : Environ.env -> evar_map

val from_ctx : UState.t -> 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.t

val add : evar_map -> Evar.t -> evar_info -> evar_map

val find : evar_map -> Evar.t -> evar_info

val find_undefined : evar_map -> Evar.t -> evar_info

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

val mem : evar_map -> Evar.t -> bool

val fold : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

val fold_undefined : (Evar.t -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a

val raw_map : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_map

val raw_map_undefined : 
  (Evar.t -> evar_info -> evar_info) ->
  evar_map ->
  evar_map

val define : Evar.t -> Constr.constr -> evar_map -> evar_map

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

val is_evar : evar_map -> Evar.t -> bool

val is_defined : evar_map -> Evar.t -> bool

val is_undefined : evar_map -> Evar.t -> bool

val add_constraints : evar_map -> Univ.Constraint.t -> 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 -> Constr.existential -> Constr.constr

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

val existential_opt_value : 
  evar_map ->
  Constr.existential ->
  Constr.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 ->
  Constr.constr ->
  Constr.constr array ->
  Constr.constr

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

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

val is_restricted_evar : evar_info -> Evar.t option

val downcast : Evar.t -> Constr.types -> evar_map -> evar_map

val evar_source : Evar.t -> evar_map -> Evar_kinds.t Loc.located

val evar_ident : Evar.t -> evar_map -> Names.Id.t option

val rename : Evar.t -> Names.Id.t -> evar_map -> evar_map

val evar_key : Names.Id.t -> evar_map -> Evar.t

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

val dependent_evar_ident : Evar.t -> 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

type goal_kind =

| ToShelve
| ToGiveUp

val declare_future_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map

val declare_principal_goal : ?tag:goal_kind -> Evar.t -> evar_map -> evar_map

val future_goals : evar_map -> Evar.t list

val principal_future_goal : evar_map -> Evar.t option

type future_goals

val save_future_goals : evar_map -> future_goals

val reset_future_goals : evar_map -> evar_map

val restore_future_goals : evar_map -> future_goals -> evar_map

val fold_future_goals : 
  (evar_map -> Evar.t -> evar_map) ->
  evar_map ->
  future_goals ->
  evar_map

val map_filter_future_goals : 
  (Evar.t -> Evar.t option) ->
  future_goals ->
  future_goals

val filter_future_goals : (Evar.t -> bool) -> future_goals -> future_goals

val dispatch_future_goals : 
  future_goals ->
  Evar.t list * Evar.t list * Evar.t list * Evar.t option

val extract_given_up_future_goals : future_goals -> Evar.t list * Evar.t list

val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals

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

exception UniversesDiffer

val add_universe_constraints : evar_map -> Universes.Constraints.t -> 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 : Constr.constr -> Metaset.t

val mk_freelisted : Constr.constr -> Constr.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 * Constr.constr freelisted
| Clval of Names.Name.t * Constr.constr freelisted * instance_status * Constr.constr freelisted

type conv_pb = Reduction.conv_pb

type evar_constraint = conv_pb * Environ.env * Constr.constr * Constr.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 : Constr.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 -> (Constr.metavariable * clbinding) list

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

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

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

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

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

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

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

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

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

val meta_reassign : 
  Constr.metavariable ->
  (Constr.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 -> Constr.metavariable list

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

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

type metabinding = Constr.metavariable * Constr.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 * UState.t

val evar_universe_context_set : UState.t -> Univ.ContextSet.t

deprecated Alias of UState.context_set

val evar_universe_context_constraints : UState.t -> Univ.Constraint.t

deprecated Alias of UState.constraints

val evar_context_universe_context : UState.t -> Univ.UContext.t

deprecated alias of UState.context

val evar_universe_context_of : Univ.ContextSet.t -> UState.t

deprecated Alias of UState.of_context_set

val empty_evar_universe_context : UState.t

deprecated Alias of UState.empty

val union_evar_universe_context : UState.t -> UState.t -> UState.t

deprecated Alias of UState.union

val evar_universe_context_subst : UState.t -> Universes.universe_opt_subst

deprecated Alias of UState.subst

val constrain_variables : Univ.LSet.t -> UState.t -> UState.t

deprecated Alias of UState.constrain_variables

val evar_universe_context_of_binders : Universes.universe_binders -> UState.t

deprecated Alias of UState.of_binders

val make_evar_universe_context : 
  Environ.env ->
  Misctypes.lident list option ->
  UState.t

deprecated Use UState.make or UState.make_with_initial_binders

val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map

val universe_of_name : evar_map -> Names.Id.t -> Univ.Level.t

val universe_binders : evar_map -> Universes.universe_binders

val add_constraints_context : UState.t -> Univ.Constraint.t -> UState.t

deprecated Alias of UState.add_constraints

val normalize_evar_universe_context_variables : 
  UState.t ->
  Univ.universe_subst in_evar_universe_context

deprecated Alias of UState.normalize_variables

val normalize_evar_universe_context : UState.t -> UState.t

deprecated Alias of UState.minimize

val new_univ_level_variable : 
  ?loc:Loc.t ->
  ?name:Names.Id.t ->
  rigid ->
  evar_map ->
  evar_map * Univ.Level.t

val new_univ_variable : 
  ?loc:Loc.t ->
  ?name:Names.Id.t ->
  rigid ->
  evar_map ->
  evar_map * Univ.Universe.t

val new_sort_variable : 
  ?loc:Loc.t ->
  ?name:Names.Id.t ->
  rigid ->
  evar_map ->
  evar_map * Sorts.t

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.Level.t ->
  evar_map

val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option

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

val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t

val normalize_universe_instance : 
  evar_map ->
  Univ.Instance.t ->
  Univ.Instance.t

val set_leq_sort : Environ.env -> evar_map -> Sorts.t -> Sorts.t -> evar_map

val set_eq_sort : Environ.env -> evar_map -> Sorts.t -> Sorts.t -> evar_map

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

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

val set_eq_instances : 
  ?flex:bool ->
  evar_map ->
  Univ.Instance.t ->
  Univ.Instance.t ->
  evar_map

val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool

val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool

val evar_universe_context : evar_map -> UState.t

val universe_context_set : evar_map -> Univ.ContextSet.t

val universe_subst : evar_map -> Universes.universe_opt_subst

val universes : evar_map -> UGraph.t

val to_universe_context : evar_map -> Univ.UContext.t

val const_univ_entry : 
  poly:bool ->
  evar_map ->
  Entries.constant_universes_entry

val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes

val check_univ_decl : 
  poly:bool ->
  evar_map ->
  UState.universe_decl ->
  Entries.constant_universes_entry

val merge_universe_context : evar_map -> UState.t -> evar_map

val set_universe_context : evar_map -> UState.t -> evar_map

val merge_context_set : 
  ?loc:Loc.t ->
  ?sideff:bool ->
  rigid ->
  evar_map ->
  Univ.ContextSet.t ->
  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 : UState.t -> UState.t

deprecated Alias of UState.abstract_undefined_variables

val fix_undefined_variables : evar_map -> evar_map

val refresh_undefined_universes : 
  evar_map ->
  evar_map * Univ.universe_level_subst

val minimize_universes : evar_map -> evar_map

val nf_constraints : evar_map -> evar_map

deprecated Alias of Evd.minimize_universes

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

val fresh_sort_in_family : 
  ?loc:Loc.t ->
  ?rigid:rigid ->
  Environ.env ->
  evar_map ->
  Sorts.family ->
  evar_map * Sorts.t

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

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

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

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

type open_constr = evar_map * Constr.constr

type unsolvability_explanation =

| SeveralInstancesFound of int

val evar_counter_summary_tag : int Summary.Dyn.tag

val create_evar_defs : evar_map -> evar_map

package coq