coq 8.9.1 · OCaml Package

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 =

| KeepUserNameAndRenameExistingButSectionNames
| KeepUserNameAndRenameExistingEvenSectionNames
| KeepExistingNames
| 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_global : 
  Evd.evar_map ->
  Names.GlobRef.t ->
  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 judge_of_new_Type : Evd.evar_map -> Evd.evar_map * EConstr.unsafe_judgment

val whd_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr

val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr

val j_nf_evar : 
  Evd.evar_map ->
  EConstr.unsafe_judgment ->
  EConstr.unsafe_judgment

val jl_nf_evar : 
  Evd.evar_map ->
  EConstr.unsafe_judgment list ->
  EConstr.unsafe_judgment list

val jv_nf_evar : 
  Evd.evar_map ->
  EConstr.unsafe_judgment array ->
  EConstr.unsafe_judgment array

val tj_nf_evar : 
  Evd.evar_map ->
  EConstr.unsafe_type_judgment ->
  EConstr.unsafe_type_judgment

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 kind_of_term_upto : 
  Evd.evar_map ->
  Constr.constr ->
  (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term

val eq_constr_univs_test : 
  Evd.evar_map ->
  Evd.evar_map ->
  EConstr.constr ->
  EConstr.constr ->
  bool

val compare_cumulative_instances : 
  Reduction.conv_pb ->
  Univ.Variance.t array ->
  Univ.Instance.t ->
  Univ.Instance.t ->
  Evd.evar_map ->
  (Evd.evar_map, Univ.univ_inconsistency) Util.union

val compare_constructor_instances : 
  Evd.evar_map ->
  Univ.Instance.t ->
  Univ.Instance.t ->
  Evd.evar_map

type unification_pb =
  Evd.conv_pb * Environ.env * EConstr.constr * EConstr.constr

val add_unification_pb : 
  ?tail:bool ->
  unification_pb ->
  Evd.evar_map ->
  Evd.evar_map

type clear_dependency_error =

| OccurHypInSimpleClause of Names.Id.t option
| EvarTypingBreak of Constr.existential
| 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

val clear_hyps_in_evi : 
  Environ.env ->
  Evd.evar_map ->
  Environ.named_context_val ->
  EConstr.types ->
  Names.Id.Set.t ->
  Evd.evar_map * Environ.named_context_val * EConstr.types

val clear_hyps2_in_evi : 
  Environ.env ->
  Evd.evar_map ->
  Environ.named_context_val ->
  EConstr.types ->
  EConstr.types ->
  Names.Id.Set.t ->
  Evd.evar_map * Environ.named_context_val * EConstr.types * EConstr.types

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 subterm_source : 
  Evar.t ->
  ?where:Evar_kinds.subevar_kind ->
  Evar_kinds.t Loc.located ->
  Evar_kinds.t Loc.located

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]

val e_new_global : Evd.evar_map ref -> Names.GlobRef.t -> EConstr.constr

deprecated Use [Evarutil.new_global]

val e_nf_evars_and_universes : 
  Evd.evar_map ref ->
  (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst

deprecated Use Evd.minimize_universes and nf_evars_universes

package coq