Merge branch 'v8.6'

3 files changed, 35 insertions, 31 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 50c5b354ef..13444cb379 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -667,6 +667,28 @@ let gather_dependent_evars evm l =
 
 (* /spiwack *)
 
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+    the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially)
+    solved. *)
+(* spiwack: [advance] is probably performance critical, and the good
+   behaviour of its definition may depend sensitively to the actual
+   definition of [Evd.find]. Currently, [Evd.find] starts looking for
+   a value in the heap of undefined variable, which is small. Hence in
+   the most common case, where [advance] is applied to an unsolved
+   goal ([advance] is used to figure if a side effect has modified the
+   goal) it terminates quickly. *)
+let rec advance sigma evk =
+  let evi = Evd.find sigma evk in
+  match evi.evar_body with
+  | Evar_empty -> Some evk
+  | Evar_defined v ->
+      if Option.default false (Store.get evi.evar_extra cleared) then
+        let (evk,_) = Term.destEvar v in
+        advance sigma evk
+      else
+        None
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c0c81442d5..7fdc7aac78 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -110,6 +110,12 @@ val is_ground_env  :  evar_map -> env -> bool
     its (partial) definition. *)
 val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t
 
+(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+    the current avatar of [g] (for instance [g] was changed by [clear]
+    into [g']). It returns [None] if [g] has been (partially)
+    solved. *)
+val advance : evar_map -> evar -> evar option
+
 (** The following functions return the set of undefined evars
     contained in the object, the defined evars being traversed.
     This is roughly a combination of the previous functions and
diff --git a/engine/proofview.ml b/engine/proofview.ml
index d7fb651264..333ae78b3a 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -152,33 +152,9 @@ let focus i j sp =
   let (new_comb, context) = focus_sublist i j sp.comb in
   ( { sp with comb = new_comb } , context )
 
-
-(** [advance sigma g] returns [Some g'] if [g'] is undefined and is
-    the current avatar of [g] (for instance [g] was changed by [clear]
-    into [g']). It returns [None] if [g] has been (partially)
-    solved. *)
-(* spiwack: [advance] is probably performance critical, and the good
-   behaviour of its definition may depend sensitively to the actual
-   definition of [Evd.find]. Currently, [Evd.find] starts looking for
-   a value in the heap of undefined variable, which is small. Hence in
-   the most common case, where [advance] is applied to an unsolved
-   goal ([advance] is used to figure if a side effect has modified the
-   goal) it terminates quickly. *)
-let rec advance sigma g =
-  let open Evd in
-  let evi = Evd.find sigma g in
-  match evi.evar_body with
-  | Evar_empty -> Some g
-  | Evar_defined v ->
-      if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then
-        let (e,_) = Term.destEvar v in
-        advance sigma e
-      else
-        None
-
 (** [undefined defs l] is the list of goals in [l] which are still
     unsolved (after advancing cleared goals). *)
-let undefined defs l = CList.map_filter (advance defs) l
+let undefined defs l = CList.map_filter (Evarutil.advance defs) l
 
 (** Unfocuses a proofview with respect to a context. *)
 let unfocus c sp =
@@ -465,7 +441,7 @@ let iter_goal i =
   Comb.get >>= fun initial ->
   Proof.List.fold_left begin fun (subgoals as cur) goal ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -489,7 +465,7 @@ let fold_left2_goal i s l =
   in 
   Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a ->
     Solution.get >>= fun step ->
-    match advance step goal with
+    match Evarutil.advance step goal with
     | None -> return cur
     | Some goal ->
         Comb.set [goal] >>
@@ -533,7 +509,7 @@ let tclDISPATCHGEN0 join tacs =
         let open Proof in
         Pv.get >>= function
         | { comb=[goal] ; solution } ->
-            begin match advance solution goal with
+            begin match Evarutil.advance solution goal with
             | None -> tclUNIT (join [])
             | Some _ -> Proof.map (fun res -> join [res]) tac
             end
@@ -965,7 +941,7 @@ module Unsafe = struct
   let mark_as_goal evd content =
     mark_in_evm ~goal:true evd content
 
-  let advance = advance
+  let advance = Evarutil.advance
 
   let mark_as_unresolvable p gl =
     { p with solution = mark_in_evm ~goal:false p.solution gl }
@@ -1130,7 +1106,7 @@ module Goal = struct
     Pv.get >>= fun step ->
     let sigma = step.solution in
     let map goal =
-      match advance sigma goal with
+      match Evarutil.advance sigma goal with
       | None -> None (** ppedrot: Is this check really necessary? *)
       | Some goal ->
         let gl =
@@ -1144,7 +1120,7 @@ module Goal = struct
 
   let unsolved { self=self } =
     tclEVARMAP >>= fun sigma ->
-    tclUNIT (not (Option.is_empty (advance sigma self)))
+    tclUNIT (not (Option.is_empty (Evarutil.advance sigma self)))
 
   (* compatibility *)
   let goal { self=self } = self