diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-28 16:34:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-28 16:34:48 +0000 |
| commit | b1a7fc5c5180b112a0bee5617f314bee34283092 (patch) | |
| tree | 24540bb96016eb4fa4f1809836577ccebfc53629 /test-suite/parser | |
| parent | a7898ee7af61c9dc743ecb0faa68759e545c1d53 (diff) | |
Passage à la v8 pour test parser
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6367 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/parser')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 22 |
1 files changed, 1 insertions, 21 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index aeb975b59..bff7b3425 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 |