From 1e095dd3f8b61a50dfd19f72d12e37a26a64435a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 15 May 2005 12:48:57 +0000
Subject: Allow auto to have a parametric argument (wish #967)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tacticnew.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/g_tacticnew.ml4')

diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index c41de337b0..c7fee72db6 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -346,7 +346,7 @@ GEXTEND Gram
 
       (* Automation tactic *)
       | IDENT "trivial"; db = hintbases -> TacTrivial db
-      | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
+      | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
 
 (* Obsolete since V8.0
       | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
@@ -355,7 +355,7 @@ GEXTEND Gram
       | IDENT "dconcl"  -> TacDestructConcl
       | IDENT "superauto"; l = autoargs -> TacSuperAuto l
 *)
-      | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
+      | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural ->
 	  TacDAuto (n, p)
 
       (* Context management *)
-- 
cgit v1.2.3