package coq

  1. Overview
  2. Docs
Package contains no libraries
val string_of_existential : evar -> string
module Filter : sig ... end
type evar_body =
  1. | Evar_empty
  2. | Evar_defined of Term.constr
module Store : Store.S
type evar_info = {
  1. evar_concl : Term.constr;
  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 : Term.constr list option;
  7. evar_extra : Store.t;
}
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_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 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 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_ident : Term.existential_key -> evar_map -> Names.Id.t option
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 = {
  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 : Term.constr -> Metaset.t
val mk_freelisted : Term.constr -> Term.constr 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 * 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_opt_fvalue : evar_map -> Term.metavariable -> (Term.constr freelisted * instance_status) option
val meta_type : evar_map -> Term.metavariable -> Term.types
val meta_declare : Term.metavariable -> Term.types -> ?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 -> 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
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 * 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 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 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 =
  1. | SeveralInstancesFound of int
val create_evar_defs : evar_map -> evar_map
val evar_counter_summary_name : string
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct