Merge PR #12645: Cleanup Evarutil API

Reviewed-by: ejgallego
Reviewed-by: herbelin

9 files changed, 31 insertions, 79 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 423af1d4ec..b4b2032dd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -409,15 +409,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let new_pure_evar_full evd ?typeclass_candidate evi =
-  let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
-  let evd = Evd.declare_future_goal evk evd in
-  (evd, evk)
-
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
-    ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ =
-  let default_naming = IntroAnonymous in
-  let naming = Option.default default_naming naming in
+let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity)
+    ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ =
   let name = match naming with
   | IntroAnonymous -> None
   | IntroIdentifier id -> Some id
@@ -443,22 +436,6 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_ar
   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)
-
-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
@@ -470,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 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
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/proofs/goal.ml b/proofs/goal.ml
index 53d3047bc7..beeaa60433 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -58,15 +58,9 @@ module V82 = struct
        goals are restored to their initial value after the evar is
        created. *)
     let prev_future_goals = Evd.save_future_goals evars in
-    let evi = { Evd.evar_hyps = hyps;
-                Evd.evar_concl = concl;
-                Evd.evar_filter = Evd.Filter.identity;
-                Evd.evar_abstract_arguments = Evd.Abstraction.identity;
-                Evd.evar_body = Evd.Evar_empty;
-                Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
-                Evd.evar_candidates = None }
+    let (evars, evk) =
+      Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false hyps evars concl
     in
-    let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in
     let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = List.map (NamedDecl.get_id %> EConstr.mkVar) ctxt in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4804822c99..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
 
@@ -436,6 +437,11 @@ 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
+  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 ->
     let env = Proofview.Goal.env gl in
@@ -457,8 +463,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)