coq 8.12.2 · OCaml Package

type econstr

type etypes = econstr

module Filter : sig ... end

module Abstraction : sig ... end

type evar_body =

| Evar_empty
| Evar_defined of econstr

type evar_info = {

evar_concl : econstr;
evar_hyps : Environ.named_context_val;
evar_body : evar_body;
evar_filter : Filter.t;
evar_abstract_arguments : Abstraction.t;
evar_source : Evar_kinds.t Loc.located;
evar_candidates : econstr list option;

}

val make_evar : Environ.named_context_val -> etypes -> evar_info

val evar_concl : evar_info -> econstr

val evar_context : evar_info -> (econstr, etypes) Context.Named.pt

val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt

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_candidates : evar_info -> Constr.constr list option

val evar_filter : evar_info -> Filter.t

val evar_env : Environ.env -> evar_info -> Environ.env

val evar_filtered_env : Environ.env -> evar_info -> Environ.env

val map_evar_body : (econstr -> econstr) -> evar_body -> evar_body

val map_evar_info : (econstr -> econstr) -> evar_info -> evar_info

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 ->
  ?typeclass_candidate:bool ->
  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 -> econstr -> evar_map -> evar_map

val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map

val cmap : (econstr -> econstr) -> 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

val is_maybe_typeclass_hook : (evar_map -> Constr.constr -> bool) Hook.t

exception NotInstantiatedEvar

val existential_value : evar_map -> econstr Constr.pexistential -> econstr

val existential_value0 : evar_map -> Constr.existential -> Constr.constr

val existential_type : evar_map -> econstr Constr.pexistential -> etypes

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

val existential_opt_value : 
  evar_map ->
  econstr Constr.pexistential ->
  econstr option

val existential_opt_value0 : 
  evar_map ->
  Constr.existential ->
  Constr.constr option

val evar_instance_array : 
  (Constr.named_declaration -> 'a -> bool) ->
  evar_info ->
  'a list ->
  (Names.Id.t * 'a) list

val instantiate_evar_array : evar_info -> econstr -> econstr list -> econstr

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

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

val is_restricted_evar : evar_map -> Evar.t -> Evar.t option

val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map

val get_typeclass_evars : evar_map -> Evar.Set.t

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

val get_obligation_evars : evar_map -> Evar.Set.t

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

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

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

type side_effect_role =

| Schema of Names.inductive * string

type side_effects = {

seff_private : Safe_typing.private_constants;
seff_roles : side_effect_role Names.Cmap.t;

}

val empty_side_effects : side_effects

val concat_side_effects : side_effects -> side_effects -> side_effects

val emit_side_effects : side_effects -> evar_map -> evar_map

val eval_side_effects : evar_map -> side_effects

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

exception UniversesDiffer

val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map

module Store : Store.S

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 : econstr -> Metaset.t

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

type conv_pb = Reduction.conv_pb

type evar_constraint = conv_pb * Environ.env * econstr * econstr

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

val conv_pbs : evar_map -> evar_constraint list

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 : evar_map -> econstr -> Evar.Set.t

val evar_nodes_of_term : econstr -> Evar.Set.t

val evars_of_named_context : 
  evar_map ->
  (econstr, etypes) Context.Named.pt ->
  Evar.Set.t

val evars_of_filtered_evar_info : evar_map -> 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 -> econstr

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

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

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

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

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

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

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

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

val meta_reassign : 
  Constr.metavariable ->
  (econstr * 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 : (econstr -> econstr) -> evar_map -> evar_map

val map_metas : (econstr -> econstr) -> evar_map -> evar_map

type metabinding = Constr.metavariable * econstr * 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 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 -> UnivNames.universe_binders

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 make_nonalgebraic_variable : evar_map -> 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 check_constraints : evar_map -> Univ.Constraint.t -> bool

val evar_universe_context : evar_map -> UState.t

val universe_context_set : evar_map -> Univ.ContextSet.t

val universe_subst : evar_map -> UnivSubst.universe_opt_subst

val universes : evar_map -> UGraph.t

val to_universe_context : evar_map -> Univ.UContext.t

val univ_entry : poly:bool -> evar_map -> Entries.universes_entry

val check_univ_decl : 
  poly:bool ->
  evar_map ->
  UState.universe_decl ->
  Entries.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 -> UnivSubst.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 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 update_sigma_env : evar_map -> Environ.env -> evar_map

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

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

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

val fresh_constructor_instance : 
  ?loc:Loc.t ->
  ?rigid:rigid ->
  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 ->
  Names.GlobRef.t ->
  evar_map * econstr

type open_constr = evar_map * econstr

type unsolvability_explanation =

| SeveralInstancesFound of int

val evar_counter_summary_tag : int Summary.Dyn.tag

val create_evar_defs : evar_map -> evar_map

module MiniEConstr : sig ... end

package coq