From dc7f5e8bbd6fb7da277ee89278211105157b2041 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 19 Feb 2007 22:37:24 +0000
Subject: Correct coq depend, add eq_rect elimination tactic to SubtacTactics

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9661 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/subtac/SubtacTactics.v | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'contrib')

diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v
index 17ebb44117..8c8f7c43ac 100644
--- a/contrib/subtac/SubtacTactics.v
+++ b/contrib/subtac/SubtacTactics.v
@@ -73,3 +73,11 @@ Ltac bang :=
         | context [False_rect _ ?p] => elim p
       end
   end.
+
+Ltac elim_eq_rect :=
+  match goal with
+    | [ |- ?t ] => 
+      match t with
+        context [ @eq_rect _ _ _ _ _ ?p ] => try case p ; simpl
+      end
+  end.
-- 
cgit v1.2.3