From b1a7fc5c5180b112a0bee5617f314bee34283092 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 28 Nov 2004 16:34:48 +0000
Subject: Passage à la v8 pour test parser

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

diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
index aeb975b59a..bff7b3425b 100644
--- a/test-suite/parser/obj_magic.v
+++ b/test-suite/parser/obj_magic.v
@@ -1,21 +1 @@
-Inversion H.
-Absurd (Ex [a:b] c).
-Discriminate H.
-DEq 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).
-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) ] in v.
-Hint Rewrite <- [ (A b) ] in v using Auto.
+inversion H.
\ No newline at end of file
-- 
cgit v1.2.3