package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val new_meta : unit -> Constr.metavariable
val mk_new_meta : unit -> EConstr.constr
val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.t
type naming_mode =
  1. | KeepUserNameAndRenameExistingButSectionNames
  2. | KeepUserNameAndRenameExistingEvenSectionNames
  3. | KeepExistingNames
  4. | FailIfConflict
val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?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 -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> Evd.evar_map * Evar.t
val new_pure_evar_full : Evd.evar_map -> Evd.evar_info -> 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 new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> Environ.named_context_val -> Evd.evar_map -> EConstr.types -> EConstr.constr list -> Evd.evar_map * EConstr.constr
val make_pure_subst : Evd.evar_info -> 'a array -> (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 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
val nf_evars_and_universes : Evd.evar_map -> Evd.evar_map * (Constr.constr -> Constr.constr)
  • deprecated Use Evd.minimize_universes and nf_evars_universes
val nf_evar_map_universes : Evd.evar_map -> Evd.evar_map * (Constr.constr -> Constr.constr)
  • deprecated Use Evd.minimize_universes and nf_evar_map and nf_evars_universes
exception Uninstantiated_evar of Evar.t
val flush_and_check_evars : Evd.evar_map -> EConstr.constr -> Constr.constr
val eq_constr_univs_test : Evd.evar_map -> 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 * EConstr.named_context
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 evd_comb0 : (Evd.evar_map -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'a
val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a
val evd_comb2 : (Evd.evar_map -> 'b -> 'c -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'c -> 'a
val meta_counter_summary_tag : int Summary.Dyn.tag
val e_new_evar : Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?candidates:EConstr.constr list -> ?store:Evd.Store.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> EConstr.types -> EConstr.constr
  • deprecated Use [Evarutil.new_evar]
val e_new_type_evar : Environ.env -> Evd.evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Namegen.intro_pattern_naming_expr -> ?principal:bool -> ?hypnaming:naming_mode -> Evd.rigid -> EConstr.constr * Sorts.t
  • deprecated Use [Evarutil.new_type_evar]
val e_new_Type : ?rigid:Evd.rigid -> Evd.evar_map ref -> EConstr.constr
  • deprecated Use [Evarutil.new_Type]
  • deprecated Use [Evarutil.new_global]
  • deprecated Use Evd.minimize_universes and nf_evars_universes