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".

---
 theories/Init/Logic.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'theories')

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