package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val new_meta : unit -> Constr.metavariable
type naming_mode =
  1. | KeepUserNameAndRenameExistingButSectionNames
  2. | KeepUserNameAndRenameExistingEvenSectionNames
  3. | KeepExistingNames
  4. | FailIfConflict
  5. | ProgramNaming
val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.t
val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?identity:EConstr.t list -> ?abstract_arguments:Evd.Abstraction.t -> ?candidates:EConstr.constr list -> ?naming:Namegen.intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * Evar.t
val new_type_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> Evd.rigid -> Evd.evar_map * (EConstr.constr * Sorts.t)
val new_Type : ?rigid:Evd.rigid -> Evd.evar_map -> Evd.evar_map * EConstr.constr
val make_pure_subst : Evd.evar_info -> 'a list -> (Names.Id.t * 'a) list
val safe_evar_value : Evd.evar_map -> Constr.existential -> Constr.constr option
val non_instantiated : Evd.evar_map -> Evd.evar_info Evar.Map.t
exception NoHeadEvar
val head_evar : Evd.evar_map -> EConstr.constr -> Evar.t
val whd_head_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr
val has_undefined_evars : Evd.evar_map -> EConstr.constr -> bool
val is_ground_term : Evd.evar_map -> EConstr.constr -> bool
val is_ground_env : Evd.evar_map -> Environ.env -> bool
val gather_dependent_evars : Evd.evar_map -> Evar.t list -> Evar.Set.t option Evar.Map.t
val advance : Evd.evar_map -> Evar.t -> Evar.t option
val reachable_from_evars : Evd.evar_map -> Evar.Set.t -> Evar.Set.t
val undefined_evars_of_term : Evd.evar_map -> EConstr.constr -> Evar.Set.t
val undefined_evars_of_named_context : Evd.evar_map -> Constr.named_context -> Evar.Set.t
val undefined_evars_of_evar_info : Evd.evar_map -> Evd.evar_info -> Evar.Set.t
type undefined_evars_cache
val create_undefined_evars_cache : unit -> undefined_evars_cache
val filtered_undefined_evars_of_evar_info : ?cache:undefined_evars_cache -> Evd.evar_map -> Evd.evar_info -> Evar.Set.t
val occur_evar_upto : Evd.evar_map -> Evar.t -> EConstr.constr -> bool
val nf_named_context_evar : Evd.evar_map -> Constr.named_context -> Constr.named_context
val nf_rel_context_evar : Evd.evar_map -> EConstr.rel_context -> EConstr.rel_context
val nf_env_evar : Evd.evar_map -> Environ.env -> Environ.env
val nf_evar_info : Evd.evar_map -> Evd.evar_info -> Evd.evar_info
val nf_evar_map : Evd.evar_map -> Evd.evar_map
val nf_evar_map_undefined : Evd.evar_map -> Evd.evar_map
val nf_evars_universes : Evd.evar_map -> Constr.constr -> Constr.constr
exception Uninstantiated_evar of Evar.t
val flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
val finalize : ?abort_on_undefined_evars:bool -> Evd.evar_map -> ((EConstr.t -> Constr.t) -> 'a) -> Evd.evar_map * 'a
val eq_constr_univs_test : evd:Evd.evar_map -> extended_evd:Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
val compare_constructor_instances : Evd.evar_map -> Univ.Instance.t -> Univ.Instance.t -> Evd.evar_map
val add_unification_pb : ?tail:bool -> unification_pb -> Evd.evar_map -> Evd.evar_map
type clear_dependency_error =
  1. | OccurHypInSimpleClause of Names.Id.t option
  2. | EvarTypingBreak of Constr.existential
  3. | NoCandidatesLeft of Evar.t
exception ClearDependencyError of Names.Id.t * clear_dependency_error * Names.GlobRef.t option
val restrict_evar : Evd.evar_map -> Evar.t -> Evd.Filter.t -> ?src:Evar_kinds.t Loc.located -> EConstr.constr list option -> Evd.evar_map * Evar.t
type csubst
val empty_csubst : csubst
val csubst_subst : csubst -> EConstr.constr -> EConstr.constr
type ext_named_context = csubst * Names.Id.Set.t * Environ.named_context_val
val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> Evd.evar_map -> EConstr.rel_declaration -> ext_named_context -> ext_named_context
val push_rel_context_to_named_context : ?hypnaming:naming_mode -> Environ.env -> Evd.evar_map -> EConstr.types -> Environ.named_context_val * EConstr.types * EConstr.constr list * csubst
val generalize_evar_over_rels : Evd.evar_map -> EConstr.existential -> EConstr.types * EConstr.constr list
val meta_counter_summary_tag : int Summary.Dyn.tag