From f6916774eea2ecc1262377cb14c2d494a0486358 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 29 Oct 2016 19:07:21 +0200
Subject: Do not shelve non-class subgoals but fail, it should

be the instance writer's responsibility to not generated non-dependent
non-class subgoals (otherwise we loose compatibility as shown in
e.g. MathClasses, which goes into loops because of unexpectedly
unconstrained goals). Reflect it in the doc.
---
 tactics/class_tactics.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 91eb388b3e..fe12b54a13 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1020,16 +1020,17 @@ module Search = struct
 	Evd.add sigma gl evi')
       sigma goals
 
-  let shelve_nonclass info =
+  let fail_if_nonclass info =
     Proofview.Goal.enter { enter = fun gl ->
       let gl = Proofview.Goal.assume gl in
       let sigma = Sigma.to_evar_map (Proofview.Goal.sigma gl) in
       if is_class_type sigma (Proofview.Goal.concl gl) then
         Proofview.tclUNIT ()
       else (if !typeclasses_debug > 1 then
-              Feedback.msg_debug (pr_depth info.search_depth ++ str": shelving non-class subgoal " ++
+              Feedback.msg_debug (pr_depth info.search_depth ++
+                                    str": failure due to non-class subgoal " ++
                                     pr_ev sigma (Proofview.Goal.goal gl));
-            Proofview.shelve) }
+            Proofview.tclZERO NotApplicableEx) }
 
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
@@ -1159,7 +1160,7 @@ module Search = struct
       if path_matches derivs [] then aux e tl
       else
         let filter =
-          if info.search_only_classes then shelve_nonclass info
+          if info.search_only_classes then fail_if_nonclass info
           else Proofview.tclUNIT ()
         in
         ortac
-- 
cgit v1.2.3