- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",

  and, with a now generic intropattern "[]", also "as []_eqn", "as []_eqn:H"
  for "destruct" with equality keeping.
- Fixed an accuracy loss in error location.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11732 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 0 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 2e0fe42b68..a59eba6f46 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -72,6 +72,17 @@ Ltac false_hyp H G :=
 
 Ltac case_eq x := generalize (refl_equal x); pattern x at -1; case x.
 
+(* Similar variants of destruct *)
+
+Tactic Notation "destruct_with_eqn" constr(x) :=
+  destruct x as []_eqn.
+Tactic Notation "destruct_with_eqn" ident(n) := 
+  try intros until n; destruct n as []_eqn.
+Tactic Notation "destruct_with_eqn" ":" ident(H) constr(x) :=
+  destruct x as []_eqn:H.
+Tactic Notation "destruct_with_eqn" ":" ident(H) ident(n) := 
+  try intros until n; destruct n as []_eqn:H.
+
 (* Rewriting in all hypothesis several times everywhere *)
 
 Tactic Notation "rewrite_all" constr(eq) := repeat rewrite eq in *.