diff options
| author | Emilio Jesus Gallego Arias | 2020-07-08 12:32:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-08 12:32:00 +0200 |
| commit | cf383c1f2e0c9effd9774bc25579eeaca4c24ae0 (patch) | |
| tree | 229f3c6023d32b09cc646ce28497f91d096cb87e /engine/evarutil.mli | |
| parent | 5331a010acbb71131bc5dc1c62cc08d9814de21b (diff) | |
| parent | 834c64015b608b8152e160d37e6f07a3106ff26b (diff) | |
Merge PR #12645: Cleanup Evarutil API
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index b3c94e6b3b..41b58d38b0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,14 +25,6 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) -val new_evar_from_context : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> - ?naming:intro_pattern_naming_expr -> - ?typeclass_candidate:bool -> - ?principal:bool -> - named_context_val -> evar_map -> types -> evar_map * EConstr.t - type naming_mode = | KeepUserNameAndRenameExistingButSectionNames | KeepUserNameAndRenameExistingEvenSectionNames @@ -56,8 +48,6 @@ val new_pure_evar : ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t -val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : @@ -73,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * 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 - [sign] and type [ty], [inst] is a mapping of the evar context to - the context where the evar should occur. This means that the terms - of [inst] are typed in the occurrence context and their type (seen - as a telescope) is [sign] *) -val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> - ?naming:intro_pattern_naming_expr -> - ?typeclass_candidate:bool -> - ?principal:bool -> - named_context_val -> evar_map -> types -> - constr list -> evar_map * constr - val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option |