Merge branch 'v8.5' into v8.6

2 files changed, 30 insertions, 15 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index f2f400515..85a52fdca 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -685,6 +685,21 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
+let mark_in_evm ~goal evd content =
+  let info = Evd.find evd content in
+  let info =
+    if goal then
+      { info with Evd.evar_source = match info.Evd.evar_source with
+            | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+            | loc,_ -> loc,Evar_kinds.GoalEvar }
+    else info
+  in
+  let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
+  | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
+  | Some () -> info
+  in
+  Evd.add evd content info
+
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
@@ -697,8 +712,11 @@ let with_shelf tac =
   let fgoals = Evd.future_goals solution in
   let pgoal = Evd.principal_future_goal solution in
   let sigma = Evd.restore_future_goals sigma fgoals pgoal in
-  Pv.set { npv with shelf; solution = sigma } >>
-  tclUNIT (CList.rev_append gls' gls, ans)
+  (* Ensure we mark and return only unsolved goals *)
+  let gls' = undefined sigma (CList.rev_append gls' gls) in
+  let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+  let npv = { npv with shelf; solution = sigma } in
+  Pv.set npv >> tclUNIT (gls', ans)
 
 (** [goodmod p m] computes the representative of [p] modulo [m] in the
     interval [[0,m-1]].*)
@@ -945,20 +963,13 @@ module Unsafe = struct
     { p with solution = Evd.reset_future_goals p.solution }
 
   let mark_as_goal evd content =
-    let info = Evd.find evd content in
-    let info =
-      { info with Evd.evar_source = match info.Evd.evar_source with
-      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-      | loc,_ -> loc,Evar_kinds.GoalEvar }
-    in
-    let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-    | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-    | Some () -> info
-    in
-    Evd.add evd content info
+    mark_in_evm ~goal:true evd content
 
   let advance = advance
 
+  let mark_as_unresolvable p gl =
+    { p with solution = mark_in_evm ~goal:false p.solution gl }
+
   let typeclass_resolvable = typeclass_resolvable
 
 end
diff --git a/engine/proofview.mli b/engine/proofview.mli
index fae75f825..725445251 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -326,8 +326,9 @@ val unshelve : Goal.goal list -> proofview -> proofview
 (** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
 val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
 
-(** [with_shelf tac] executes [tac] and returns its result together with the set
-    of goals shelved by [tac]. The current shelf is unchanged. *)
+(** [with_shelf tac] executes [tac] and returns its result together with
+    the set of goals shelved by [tac]. The current shelf is unchanged
+    and the returned list contains only unsolved goals. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
 
 (** If [n] is positive, [cycle n] puts the [n] first goal last. If [n]
@@ -434,6 +435,9 @@ module Unsafe : sig
       and makes it unresolvable for type classes. *)
   val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
 
+  (** Make an evar unresolvable for type classes. *)
+  val mark_as_unresolvable : proofview -> Evar.t -> proofview
+
   (** [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)