From a2c21128cbc71812ba9bc288f16f56a5f45bd18d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 May 2005 13:13:33 +0000
Subject: 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
---
 test-suite/parser/obj_magic.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/parser/obj_magic.v')

diff --git a/test-suite/parser/obj_magic.v b/test-suite/parser/obj_magic.v
index 6de2f8c7f3..c919d6d8d5 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.
-- 
cgit v1.2.3