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.

3 files changed, 31 insertions, 1 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