diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-28 18:20:57 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-28 18:20:57 +0000 |
| commit | d1aa8bd1fb7d1e8a8680fc6397d16e31c0f82666 (patch) | |
| tree | fa1699e69602dd7c4ff10a61b7e72d8b077ddafc /test-suite | |
| parent | a2a27316159a0a4b82db82263dc96098e0f476d2 (diff) | |
Re-commit version nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6370 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index bff7b3425..6de2f8c7f 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. |