diff options
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 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 |