Remove Evarutil.new_evar_from_context from the API.

3 files changed, 6 insertions, 18 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index e30f908df0..9bfe3e21f3 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -444,14 +444,6 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type
   let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in
   evd, mkEvar (newevk, instance)
 
-let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
-  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
-  let instance =
-    match filter with
-    | None -> instance
-    | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal 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
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c463415b6a..c592a4f5d1 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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4804822c99..7269b5c02d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -436,6 +436,10 @@ let clear_hyps2 env sigma ids sign t cl =
   with Evarutil.ClearDependencyError (id,err,inglobal) ->
     error_replacing_dependency env sigma id err inglobal
 
+let new_evar_from_context ?principal sign evd typ =
+  let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
+  Evarutil.new_evar_instance sign evd typ instance
+
 let internal_cut ?(check=true) replace id t =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
@@ -457,8 +461,8 @@ let internal_cut ?(check=true) replace id t =
     Proofview.tclTHEN
       (Proofview.Unsafe.tclEVARS sigma)
       (Refine.refine ~typecheck:false begin fun sigma ->
-        let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
-        let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
+        let (sigma, ev) = new_evar_from_context sign sigma nf_t in
+        let (sigma, ev') = new_evar_from_context sign' sigma ~principal:true concl in
         let term = mkLetIn (make_annot (Name id) r, ev, t, EConstr.Vars.subst_var id ev') in
         (sigma, term)
       end)