package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type econstr
type etypes = econstr
module Filter : sig ... end
type evar_body =
  1. | Evar_empty
  2. | Evar_defined of econstr
module Store : Store.S
type evar_info = {
  1. evar_concl : econstr;
  2. evar_hyps : Environ.named_context_val;
  3. evar_body : evar_body;
  4. evar_filter : Filter.t;
  5. evar_source : Evar_kinds.t Loc.located;
  6. evar_candidates : econstr list option;
  7. evar_extra : Store.t;
}
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_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 : evar_info -> Environ.env
val evar_filtered_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 -> 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 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
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 array -> (Names.Id.t * 'a) list
val instantiate_evar_array : evar_info -> econstr -> econstr array -> 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_info -> Evar.t option
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
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 =
  1. | ToShelve
  2. | 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
val get_extra_data : evar_map -> Store.t
val set_extra_data : Store.t -> evar_map -> evar_map
type !'a sigma = {
  1. it : 'a;
  2. 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 = {
  1. rebus : 'a;
  2. 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 =
  1. | IsSuperType
  2. | IsSubType
  3. | Conv
val eq_instance_constraint : instance_constraint -> instance_constraint -> bool
type instance_typing_status =
  1. | CoerceToType
  2. | TypeNotProcessed
  3. | TypeProcessed
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 : Constr.constr -> Evar.Set.t
val evars_of_named_context : (econstr, etypes) Context.Named.pt -> 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 -> econstr
val meta_opt_fvalue : evar_map -> Constr.metavariable -> (econstr freelisted * instance_status) option
val meta_type : evar_map -> Constr.metavariable -> etypes
val meta_declare : Constr.metavariable -> etypes -> ?name:Names.Name.t -> 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
val retract_coercible_metas : evar_map -> metabinding list * evar_map
type rigid = UState.rigid =
  1. | UnivRigid
  2. | 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 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 -> 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 -> 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 -> Names.GlobRef.t -> evar_map * econstr
type open_constr = evar_map * econstr
type unsolvability_explanation =
  1. | SeveralInstancesFound of int
val evar_counter_summary_tag : int Summary.Dyn.tag
val create_evar_defs : evar_map -> evar_map
module MiniEConstr : sig ... end