diff options
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 90 |
1 files changed, 53 insertions, 37 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 972b0b9e1..f271c14ea 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,53 +25,51 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar_from_context : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * EConstr.t + +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict val new_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * Evar.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * Evar.t val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t -(** the same with side-effects *) -val e_new_evar : - env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> - evar_map * (constr * Sorts.t) - -val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> rigid -> + evar_map * (constr * Sorts.t) val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr val restrict_evar : evar_map -> Evar.t -> Filter.t -> ?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t (** Polymorphic constants *) -val new_global : evar_map -> Globnames.global_reference -> evar_map * constr -val e_new_global : evar_map ref -> Globnames.global_reference -> constr +val new_global : evar_map -> GlobRef.t -> evar_map * constr (** Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -80,10 +78,10 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> + named_context_val -> evar_map -> types -> constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list @@ -178,11 +176,12 @@ val nf_evar_map_undefined : evar_map -> evar_map val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) -val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] (** Normalize the evar map w.r.t. universes, after simplification of constraints. Return the substitution function for constrs as well. *) val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr) +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evar_map and nf_evars_universes"] (** Replacing all evars, possibly raising [Uninstantiated_evar] *) exception Uninstantiated_evar of Evar.t @@ -201,7 +200,7 @@ val kind_of_term_upto : evar_map -> Constr.constr -> universes. The term [t] is interpreted in [sigma1] while [u] is interpreted in [sigma2]. The universe constraints in [sigma2] are assumed to be an extention of those in [sigma1]. *) -val eq_constr_univs_test : evar_map -> evar_map -> Constr.constr -> Constr.constr -> bool +val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool (** [compare_cumulative_instances cv_pb variance u1 u2 sigma] Returns [Inl sigma'] where [sigma'] is [sigma] augmented with universe @@ -224,13 +223,13 @@ type clear_dependency_error = | OccurHypInSimpleClause of Id.t option | EvarTypingBreak of Constr.existential -exception ClearDependencyError of Id.t * clear_dependency_error +exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option -val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> - Id.Set.t -> named_context_val * types +val clear_hyps_in_evi : env -> evar_map -> named_context_val -> types -> + Id.Set.t -> evar_map * named_context_val * types -val clear_hyps2_in_evi : env -> evar_map ref -> named_context_val -> types -> types -> - Id.Set.t -> named_context_val * types * types +val clear_hyps2_in_evi : env -> evar_map -> named_context_val -> types -> types -> + Id.Set.t -> evar_map * named_context_val * types * types type csubst @@ -240,10 +239,11 @@ val csubst_subst : csubst -> constr -> constr type ext_named_context = csubst * Id.Set.t * named_context -val push_rel_decl_to_named_context : +val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> +val push_rel_context_to_named_context : ?hypnaming:naming_mode -> + Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list @@ -259,8 +259,24 @@ val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Lo val meta_counter_summary_tag : int Summary.Dyn.tag -(** Deprecated *) -type type_constraint = types option -[@@ocaml.deprecated "use the version in Evardefine"] -type val_constraint = constr option -[@@ocaml.deprecated "use the version in Evardefine"] +val e_new_evar : + env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr +[@@ocaml.deprecated "Use [Evd.new_evar]"] + +val e_new_type_evar : env -> evar_map ref -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t +[@@ocaml.deprecated "Use [Evd.new_type_evar]"] + +val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +[@@ocaml.deprecated "Use [Evd.new_Type]"] + +val e_new_global : evar_map ref -> GlobRef.t -> constr +[@@ocaml.deprecated "Use [Evd.new_global]"] + +val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst +[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"] |