diff options
| author | Pierre-Marie Pédrot | 2020-07-04 20:02:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-08 00:20:42 +0200 |
| commit | 834c64015b608b8152e160d37e6f07a3106ff26b (patch) | |
| tree | bc761838af2979d760322a270930e18fea8cffe1 /engine/evarutil.mli | |
| parent | aba870c6b58b18bc1bd4711c379863a87bbf6d33 (diff) | |
Remove Evarutil.new_evar_instance from the API.
Diffstat (limited to 'engine/evarutil.mli')
| -rw-r--r-- | engine/evarutil.mli | 15 |
1 files changed, 0 insertions, 15 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c592a4f5d1..41b58d38b0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -63,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 |