Remove Evarutil.new_evar_instance from the API.

8 files changed, 22 insertions, 43 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
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 5f463f8de4..65204b7868 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1351,9 +1351,8 @@ let unsafe_intro env decl b =
     let inst = List.map (get_id %> EConstr.mkVar) (Environ.named_context env) in
     let ninst = EConstr.mkRel 1 :: inst in
     let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
-    let sigma, ev =
-      Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in
-    sigma, EConstr.mkNamedLambda_or_LetIn decl ev
+    let sigma, ev = Evarutil.new_pure_evar ~principal:true nctx sigma nb in
+    sigma, EConstr.mkNamedLambda_or_LetIn decl (EConstr.mkEvar (ev, ninst))
   end
 
 let set_decl_id id = let open Context in function
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6880383a31..400acc25b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1411,11 +1411,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
               refresh_universes ~status:Evd.univ_flexible (Some true)
                 env_evar_unf evd evty
             else evd, evty in
-          let (evd, ev) = new_evar_instance sign evd evty ~filter instance in
-          let evk = fst (destEvar evd ev) in
+          let (evd, evk) = new_pure_evar sign evd evty ~filter in
           evsref := (evk,evty,inst,prefer_abstraction)::!evsref;
           fixed := Evar.Set.add evk !fixed;
-          evd, ev
+          evd, mkEvar (evk, instance)
      in
      let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
      if debug_ho_unification () then
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 348d7c0b2f..79839099f7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -698,10 +698,9 @@ let make_projectable_subst aliases sigma evi args =
  *)
 
 let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_sign sign filter inst_in_env =
-  let (evd, evar_in_env) = new_evar_instance sign evd ty_t_in_sign ~filter ~src inst_in_env in
+  let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
   let t_in_env = whd_evar evd t_in_env in
-  let (evk, _) = destEvar evd evar_in_env in
-  let evd = define_fun env evd None (destEvar evd evar_in_env) t_in_env in
+  let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
   let ctxt = named_context_of_val sign in
   let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
   let evar_in_sign = mkEvar (evk, inst_in_sign) in
@@ -770,9 +769,9 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
     define_evar_from_virtual_equation define_fun env evd src ty_in_env
       ty_t_in_sign sign2 filter2 inst2_in_env in
   let (evd, ev2_in_sign) =
-    new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 ~src inst2_in_sign in
-  let ev2_in_env = (fst (destEvar evd ev2_in_sign), inst2_in_env) in
-  (evd, ev2_in_sign, ev2_in_env)
+    new_pure_evar sign2 evd ev2ty_in_sign ~filter:filter2 ~src in
+  let ev2_in_env = (ev2_in_sign, inst2_in_env) in
+  (evd, mkEvar (ev2_in_sign, inst2_in_sign), ev2_in_env)
 
 let restrict_upon_filter evd evk p args =
   let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 05abb86f46..81a62a7048 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -110,7 +110,8 @@ let new_evar env sigma ?src ?naming typ =
   let instance = rel_list (nb_rel env.renamed_env) inst_vars in
   let (subst, _, sign) = Lazy.force env.extra in
   let typ' = csubst_subst subst typ in
-  new_evar_instance sign sigma typ' ?src ?naming instance
+  let (sigma, evk) = new_pure_evar sign sigma typ' ?src ?naming in
+  (sigma, mkEvar (evk, instance))
 
 let new_type_evar env sigma ~src =
   let sigma, s = Evd.new_sort_variable Evd.univ_flexible_alg sigma in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 4d148756b4..9bd7ccda5d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -781,7 +781,8 @@ let make_evar_clause env sigma ?len t =
         Some (ctx, args, subst), ctx, args, subst
       | Some (ctx, args, subst) -> inst, ctx, args, subst
       in
-      let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in
+      let (sigma, ev) = new_pure_evar ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) in
+      let ev = mkEvar (ev, args) in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7269b5c02d..f553a290f9 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -120,8 +120,8 @@ let unsafe_intro env decl b =
     let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
-    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
-    (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
+    let (sigma, ev) = new_pure_evar nctx sigma nb ~principal:true in
+    (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) (mkEvar (ev, ninst)))
   end
 
 let introduction id =
@@ -340,7 +340,8 @@ let rename_hyp repl =
       let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~typecheck:false begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
+        let sigma, ev = Evarutil.new_pure_evar nctx sigma nconcl ~principal:true in
+        sigma, mkEvar (ev, instance)
       end
     end
 
@@ -438,7 +439,8 @@ let clear_hyps2 env sigma ids sign t cl =
 
 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 (evd, evk) = Evarutil.new_pure_evar sign evd typ in
+  (evd, mkEvar (evk, instance))
 
 let internal_cut ?(check=true) replace id t =
   Proofview.Goal.enter begin fun gl ->