Move the handling a new evars from the [Proofview.Refine] module to [Evd].

That way, everything in the code of pretying is made "refine"-aware. Making the abstraction stonger and integration of pretyping with interactive proof more direct.

It might create goals in a slightly different goal order in the (user level) refine tactic. Because now, the [update] primitive which used to infer an order from an [evar_map] now has the order fixed by the successive declaration with [Evarutil.new_evar] (and similar). It probably coincides, though.

Following a suggestion by Hugo.

4 files changed, 46 insertions, 20 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 2f9606b721..ca6d26f617 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -351,16 +351,19 @@ let default_source = (Loc.ghost,Evar_kinds.InternalHole)
 
 let restrict_evar evd evk filter candidates =
   let evk' = new_untyped_evar () in
-  Evd.restrict evk evk' filter ?candidates evd, evk'
+  let evd = Evd.restrict evk evk' filter ?candidates evd in
+  Evd.declare_future_goal evk' evd, evk'
 
 let new_pure_evar_full evd evi =
   let evk = new_untyped_evar () in
   let evd = Evd.add evd evk evi in
+  let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
 let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ =
   let newevk = new_untyped_evar() in
   let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
+  let evd = Evd.declare_future_goal newevk evd in
   (evd,newevk)
 
 let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance =
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 05ab115ca6..c592ab9a54 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -585,6 +585,8 @@ type evar_map = {
   metas      : clbinding Metamap.t;
   (** Interactive proofs *)
   effects    : Declareops.side_effects;
+  future_goals : Evar.t list; (** list of newly created evars,
+                                  to be eventually turned into goals if not solved.*)
 }
 
 (*** Lifting primitive from Evar.Map. ***)
@@ -793,6 +795,7 @@ let empty = {
   metas      = Metamap.empty;
   effects    = Declareops.no_seff;
   evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+  future_goals = [];
 }
 
 let from_env ?ctx e = 
@@ -977,6 +980,15 @@ let drop_side_effects evd =
 
 let eval_side_effects evd = evd.effects
 
+(* Future goals *)
+let declare_future_goal evk evd =
+  { evd with future_goals = evk::evd.future_goals }
+
+let future_goals evd = evd.future_goals
+
+let reset_future_goals evd =
+  { evd with future_goals = [] }
+
 let meta_diff ext orig = 
   Metamap.fold (fun m v acc ->
     if Metamap.mem m orig then acc
@@ -1432,6 +1444,7 @@ let set_metas evd metas = {
   metas;
   effects = evd.effects;
   evar_names = evd.evar_names;
+  future_goals = evd.future_goals;
 }
 
 let meta_list evd = metamap_to_list evd.metas
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 542e2342f2..45432de36d 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -278,6 +278,20 @@ val eval_side_effects : evar_map -> Declareops.side_effects
 val drop_side_effects : evar_map -> evar_map
 (** This should not be used. For hacking purposes. *)
 
+(** {5 Future goals} *)
+
+val declare_future_goal : Evar.t -> evar_map -> evar_map
+(** Adds an existential variable to the list of future goals. For
+    internal uses only. *)
+
+val future_goals : evar_map -> Evar.t list
+(** Retrieves the list of future goals. Used by the [refine] primitive
+    of the tactic engine. *)
+
+val reset_future_goals : evar_map -> evar_map
+(** Clears the list of future goals. Used by the [refine] primitive of
+    the tactic engine. *)
+
 (** {5 Sort variables}
 
     Evar maps also keep track of the universe constraints defined at a given
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a19fc49b97..657f6bb2e9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -959,9 +959,9 @@ end
 
 module Refine =
 struct
-  type handle = Evd.evar_map * Evar.t list * Evar.t option
+  type handle = Evd.evar_map * Evar.t option
 
-  let new_evar (evd, evs, evkmain) ?(main=false) env typ =
+  let new_evar (evd, evkmain) ?(main=false) env typ =
     let naming =
       if main then
         (* waiting for a more principled approach
@@ -976,26 +976,25 @@ struct
       | Some _ -> Errors.error "Only one main subgoal per instantiation."
       | None -> Some evk
       else evkmain in
-    let h = (evd, evk :: evs, evkmain) in
+    let h = (evd, evkmain) in
     (h, ev)
 
-  let new_evar_instance (evd, evs, evkmain) ctx typ inst =
+  let new_evar_instance (evd, evkmain) ctx typ inst =
     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
+    let h = (evd, evkmain) in
     (h, ev)
 
-  let fresh_constructor_instance (evd,evs,evkmain) env construct =
+  let fresh_constructor_instance (evd,evkmain) env construct =
     let (evd,pconstruct) = Evd.fresh_constructor_instance env evd construct in
-    (evd,evs,evkmain) , pconstruct
+    (evd,evkmain) , pconstruct
 
-  let with_type (evd,evs,evkmain) env c t =
+  let with_type (evd,evkmain) env c t =
     let my_type = Retyping.get_type_of env evd c in
     let j = Environ.make_judge c my_type in
     let (evd,j') =
       Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
     in
-    (evd,evs,evkmain) , j'.Environ.uj_val
+    (evd,evkmain) , j'.Environ.uj_val
 
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
@@ -1013,8 +1012,9 @@ struct
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
     let concl = Goal.concl gl in
-    let handle = (sigma, [], None) in
-    let ((sigma, evs, evkmain), c) = f handle in
+    let handle = (Evd.reset_future_goals sigma, None) in
+    let ((sigma, evkmain), c) = f handle in
+    let evs = Evd.future_goals sigma in
     (** Check that the introduced evars are well-typed *)
     let fold accu ev = typecheck_evar ev env accu in
     let sigma = if unsafe then sigma else List.fold_left fold sigma evs in
@@ -1027,7 +1027,7 @@ struct
     (** 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; }
+    Proof.set { solution = Evd.reset_future_goals sigma; comb; }
   end
 
   let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl ->
@@ -1037,13 +1037,9 @@ struct
     refine ~unsafe f
   end
 
-  let update (evd, gls, evkmain) f =
+  let update (evd, evkmain) f =
     let nevd, ans = f evd in
-    let fold ev _ accu =
-      if not (Evd.mem evd ev) then ev :: accu else accu
-    in
-    let gls = Evd.fold_undefined fold nevd gls in
-    (nevd, gls, evkmain), ans
+    (nevd, evkmain), ans
 
 end