From 40323e4258d5232226d0be277f53bb5462bac417 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Sep 2019 11:41:28 +0200
Subject: Fix refine and eapply to mark shelved goals as non-resolvable, always

Check that we don't regress on PR #10762 example

Fix regression discovered by Arthur in PR #10762

Fix script of #10298 which was relying on breaking semantics for `eapply`

Add doc

Add comment in clenvtac

Actually, always mark shelved goals as unresolvable

Update doc to reflect semantics w.r.t. shelved subgoals
---
 proofs/clenvtac.ml | 4 +++-
 proofs/proof.ml    | 7 +------
 proofs/refine.ml   | 1 +
 proofs/refine.mli  | 3 ++-
 4 files changed, 7 insertions(+), 8 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 611671255d..c6a0299cf3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -72,7 +72,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
         Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
           ~fail:(not with_evars) clenv.env clenv.evd
       in
-      Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
+      (* After an apply, all the subgoals including those dependent shelved ones are in
+         the hands of the user and resolution won't be called implicitely on them. *)
+      Typeclasses.make_unresolvables (fun x -> true) evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2ee006631a..e9f93d0c8f 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,12 +386,7 @@ let run_tactic env tac pr =
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
   let shelf = (undef sigma pr.shelf)@retrieved@to_shelve in
-  let proofview =
-    List.fold_left
-      Proofview.Unsafe.mark_as_unresolvable
-      proofview
-      to_shelve
-  in
+  let proofview = Proofview.Unsafe.mark_as_unresolvables 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),result
diff --git a/proofs/refine.ml b/proofs/refine.ml
index dd8b52e56c..ea42218aaa 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -94,6 +94,7 @@ let generic_refine ~typecheck f gl =
   in
   (* Mark goals *)
   let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
+  let sigma = Proofview.Unsafe.mark_unresolvables sigma shelf in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace env sigma = Pp.(hov 2 (str"simple refine"++spc()++
                                    Termops.Internal.print_constr_env env sigma c)) in
diff --git a/proofs/refine.mli b/proofs/refine.mli
index bdcccae805..269382489d 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -25,7 +25,8 @@ val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> uni
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
     raised during the interpretation of [t] are caught and result in
-    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
+    tactic failures. If [typecheck] is [true] [t] is type-checked beforehand.
+    Shelved evars and goals are all marked as unresolvable for typeclasses. *)
 
 val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
   Proofview.Goal.t -> 'a tactic
-- 
cgit v1.2.3