Make sure the goals on the shelve are identified as goal and unresolvable for typeclasses.

This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.

Fixes #3841.

3 files changed, 33 insertions, 18 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8dc9184b8..ca98af977 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -322,15 +322,23 @@ let compact p =
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) = Proofview.apply env tac sp in
-  let shelf =
-    let sigma = Proofview.return tacticced_proofview in
-    let pre_shelf = pr.shelf@(List.rev (Evd.future_goals sigma))@to_shelve in
-    (* avoid already to count already solved goals as shelved. *)
-    List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf
+  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
+    Proofview.apply env tac sp
+  in
+  let sigma = Proofview.return tacticced_proofview in
+  (* Already solved goals are not to be counted as shelved. Nor are
+     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 proofview =
+    List.fold_left
+      Proofview.Unsafe.mark_as_goal
+      tacticced_proofview
+      retrieved
   in
   let given_up = pr.given_up@give_up in
-  let proofview = Proofview.Unsafe.reset_future_goals tacticced_proofview in
+  let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)
 
 (*** Commands ***)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index ff0e57be2..01bb41ad3 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -815,6 +815,19 @@ 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 }
+
 end
 
 
@@ -937,16 +950,6 @@ end
 module Refine =
 struct
 
-  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 = Typeclasses.mark_unresolvable info in
-    Evd.add evd content info
-
   let typecheck_evar ev env sigma =
     let info = Evd.find sigma ev in
     let evdref = ref sigma in
@@ -995,7 +998,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 mark_as_goal sigma comb in
+    let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
     let open Proof in
     InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
     Pv.set { solution = sigma; comb; }
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7e755d23d..eb54ba3ae 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -392,6 +392,10 @@ module Unsafe : sig
 
   (** Clears the future goals store in the proof view. *)
   val reset_future_goals : proofview -> proofview
+
+  (** 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
 end
 
 (** {7 Notations} *)