diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-23 13:13:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-23 13:13:33 +0000 |
| commit | a2c21128cbc71812ba9bc288f16f56a5f45bd18d (patch) | |
| tree | 71001fc0f510b251a42109c0f30c9dcbdc7dab59 /test-suite | |
| parent | 1087681cad473bdf3ef455d06beb65b7e7625f3d (diff) | |
Consequence of allowing the numerical argument of auto to be an ident for ltac
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7062 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/parser/obj_magic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v index 6de2f8c7f..c919d6d8d 100644 --- a/test-suite/parser/obj_magic.v +++ b/test-suite/parser/obj_magic.v @@ -6,8 +6,8 @@ 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. +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. |