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

1 files changed, 8 insertions, 0 deletions

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.