From d1aa8bd1fb7d1e8a8680fc6397d16e31c0f82666 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 28 Nov 2004 18:20:57 +0000
Subject: Re-commit version nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6370 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/parser/obj_magic.v | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
index bff7b3425b..6de2f8c7f3 100644
--- a/test-suite/parser/obj_magic.v
+++ b/test-suite/parser/obj_magic.v
@@ -1 +1,22 @@
-inversion H.
\ No newline at end of file
+inversion H.
+ry absurd (exists a : b, c).
+discriminate H.
+simplify_eq H.
+injection H.
+replace a with b.
+rewrite <- H with (a := b).
+rewrite <- H with (a := b) in H1.
+conditional auto rewrite H with (1 := b).
+conditional auto rewrite H with (1 := b) in H2.
+dependent rewrite H.
+cutrewrite (a = b).
+cutrewrite (a = b) in H.
+eauto 3 4 with a.
+prolog [ A (B c) ] 4.
+eapply H with (1 := H2) (a := b).
+inversion H using (A b).
+inversion H using (A b) in H1 H2.
+ring a b.
+
+Hint Rewrite -> (A b) : v.
+Hint Rewrite <- (A b) using auto : v.
-- 
cgit v1.2.3