From d226adf01f20ea946bbeac4d4c5cde75a4d77f32 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 11 Oct 2016 11:57:46 +0200
Subject: Fix bug #5123: mark all shelved evars unresolvable

Previously, some splipped through and were caught by unrelated calls to
typeclass resolution.
---
 proofs/proof.ml      |  9 ++++++++-
 proofs/proofview.ml  | 36 ++++++++++++++++++++++--------------
 proofs/proofview.mli |  8 ++++++--
 3 files changed, 36 insertions(+), 17 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 0489305aa..1f094b339 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -343,13 +343,20 @@ let run_tactic env tac pr =
      they to be marked as unresolvable. *)
   let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
+  let to_shelve = undef to_shelve in
+  let shelf = (undef pr.shelf)@retrieved@to_shelve in
   let proofview =
     List.fold_left
       Proofview.Unsafe.mark_as_goal
       tacticced_proofview
       retrieved
   in
+  let proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_unresolvable
+      proofview
+      to_shelve
+  in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ae7e2b79a..d166f46b2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -642,6 +642,18 @@ 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 = Typeclasses.mark_unresolvable info in
+  Evd.add evd content info
+
 let with_shelf tac =
   let open Proof in
   Pv.get >>= fun pv ->
@@ -654,8 +666,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]].*)
@@ -893,18 +908,11 @@ module Unsafe = struct
   let reset_future_goals p =
     { p with solution = Evd.reset_future_goals p.solution }
 
-  let mark_as_goal_evm 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 = Typeclasses.mark_unresolvable info in
-    Evd.add evd content info
-
   let mark_as_goal p gl =
-    { p with solution = mark_as_goal_evm p.solution gl }
+    { p with solution = mark_in_evm ~goal:true p.solution gl }
+
+  let mark_as_unresolvable p gl =
+    { p with solution = mark_in_evm ~goal:false p.solution gl }
 
 end
 
@@ -1107,7 +1115,7 @@ struct
     let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
     (** Select the goals *)
     let comb = undefined sigma (CList.rev evs) in
-    let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
+    let sigma = CList.fold_left (mark_in_evm ~goal:true) sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
     Pv.modify (fun ps -> { ps with solution = sigma; comb; })
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 1a367f4ea..c8d96fe79 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -303,8 +303,9 @@ val guard_no_unifiable : unit tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
-(** [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]
@@ -407,6 +408,9 @@ module Unsafe : sig
   (** Give an evar the status of a goal (changes its source location
       and makes it unresolvable for type classes. *)
   val mark_as_goal : proofview -> Evar.t -> proofview
+
+  (** Make an evar unresolvable for type classes. *)
+  val mark_as_unresolvable : proofview -> Evar.t -> proofview
 end
 
 (** {7 Notations} *)
-- 
cgit v1.2.3