Proofview.Refine: delay the marking of new evars as goals from [new_evar] to [refine].

This makes [new_evar] closer to be a mere wrapper around [Evarutil.new_evars]. Will allow restructuring of the refinement interface.

3 files changed, 12 insertions, 8 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4a1b6bfc0..ea0d534c1 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -49,6 +49,11 @@ let build e =
     cache = Evd.empty;
   }
 
+let mark_as_goal evd { content } =
+  let info = Evd.find evd content in
+  let info = { info with Evd.evar_source = (fst (info.Evd.evar_source),Evar_kinds.GoalEvar) } in
+  let info = Typeclasses.mark_unresolvable info in
+  Evd.add evd content info
 
 let uid {content = e} = string_of_int (Evar.repr e)
 let get_by_uid u =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index d04861c12..1be315c54 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -15,6 +15,8 @@ type goal
     sort of communication pipes. But I find it heavy. *)
 val build : Evd.evar -> goal 
 
+val mark_as_goal : Evd.evar_map -> goal -> Evd.evar_map
+
 (* Gives a unique identifier to each goal. The identifier is
    guaranteed to contain no space. *)
 val uid : goal -> string
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a30175de1..a19fc49b9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -870,6 +870,7 @@ end
 
 type goal = Goal.goal
 let build_goal = Goal.build
+let mark_as_goal = Goal.mark_as_goal
 let partial_solution = Goal.V82.partial_solution
 let partial_solution_to = Goal.V82.partial_solution_to
 
@@ -961,7 +962,6 @@ struct
   type handle = Evd.evar_map * Evar.t list * Evar.t option
 
   let new_evar (evd, evs, evkmain) ?(main=false) env typ =
-    let src = (Loc.ghost, Evar_kinds.GoalEvar) in
     let naming =
       if main then
         (* waiting for a more principled approach
@@ -969,9 +969,7 @@ struct
         Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
       else
         Misctypes.IntroAnonymous in
-    let (evd, ev) = Evarutil.new_evar env evd ~src ~naming typ in
-    let evd = Typeclasses.mark_unresolvables 
-      ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
+    let (evd, ev) = Evarutil.new_evar env evd ~naming typ in
     let (evk, _) = Term.destEvar ev in
     let evkmain =
       if main then match evkmain with
@@ -982,10 +980,7 @@ struct
     (h, ev)
 
   let new_evar_instance (evd, evs, evkmain) ctx typ inst =
-    let src = (Loc.ghost, Evar_kinds.GoalEvar) in
-    let (evd, ev) = Evarutil.new_evar_instance ctx evd ~src typ inst in
-    let evd = Typeclasses.mark_unresolvables 
-      ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
+    let (evd, ev) = Evarutil.new_evar_instance ctx evd typ inst in
     let (evk, _) = Term.destEvar ev in
     let h = (evd, evk :: evs, evkmain) in
     (h, ev)
@@ -1029,7 +1024,9 @@ struct
     let sigma = match evkmain with
       | None -> partial_solution sigma gl.Goal.self c 
       | Some evk -> partial_solution_to sigma gl.Goal.self (build_goal evk) c in
+    (** Select the goals *)
     let comb = undefined sigma (List.rev_map build_goal evs) in
+    let sigma = List.fold_left mark_as_goal sigma comb in
     Proof.set { solution = sigma; comb; }
   end