Remove Evarutil.new_evar_instance from the API.

2 files changed, 3 insertions, 25 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 9bfe3e21f3..b4b2032dd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -436,14 +436,6 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
-    ?principal sign evd typ instance =
-  let open EConstr in
-  assert (not !Flags.debug ||
-            List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
-  evd, mkEvar (newevk, instance)
-
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate
@@ -455,8 +447,9 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
-    ?typeclass_candidate ?principal instance
+  let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming
+    ?typeclass_candidate ?principal in
+  (evd, EConstr.mkEvar (evk, instance))
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
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