From 6879320384e63793ff9447d4aaddc919bac540ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Fri, 30 Mar 2018 16:12:26 +0200
Subject: tclSELECT: SelectAll never happens

---
 tactics/tacticals.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5e81e2d4b..8b8d5439b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -496,7 +496,7 @@ module New = struct
     | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
     | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
     | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
-    | Vernacexpr.SelectAll -> fun tac -> tac
+    | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
 
   (* Check that holes in arguments have been resolved *)
 
-- 
cgit v1.2.3