From 78717e3cdc53fda4f41bfa41f13872083413abc0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Nov 2014 17:02:32 +0100
Subject: Supporting "at occs" as a short-hand for "in |- * at occs" in
 "destruct".

---
 parsing/g_tactic.ml4  | 4 +++-
 theories/Init/Logic.v | 3 +--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a57720755a..e6f2af32ba 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -395,7 +395,9 @@ GEXTEND Gram
       | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
   ;
   opt_clause:
-    [ [ "in"; cl = in_clause -> Some cl | -> None ] ]
+    [ [ "in"; cl = in_clause -> Some cl
+      | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs}
+      | -> None ] ]
   ;
   concl_occ:
     [ [ "*"; occs = occs -> occs
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 6e8a405e0c..a7ed3c7f70 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -467,8 +467,7 @@ Proof.
   intros.
   unfold f_equal.
   rewrite <- (eq_trans_sym_inv_l (Hf a)).
-  pattern (f a) at 1 2 3 4 5 7 8, (Hf a) at 1 2.
-  destruct (Hf a).
+  destruct (Hf a) at 1 2.
   destruct (Hf a).
   reflexivity.
 Defined.
-- 
cgit v1.2.3