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

4 files changed, 8 insertions, 7 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 09d2117c8c..56c9cd67e4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -311,14 +311,14 @@ 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)
 
       | IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n
       | IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id)
       | IDENT "DHyp";  id = identref -> TacDestructHyp (false,id)
       | 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 *)
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 *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 52d6eb2d78..8e409a086d 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -534,7 +534,8 @@ and pr_atom1 = function
   | TacTrivial (Some []) as x -> pr_atom0 x
   | TacTrivial db -> hov 0 (str "Trivial" ++ pr_hintbases db)
   | TacAuto (None,Some []) as x -> pr_atom0 x
-  | TacAuto (n,db) -> hov 0 (str "Auto" ++ pr_opt int n ++ pr_hintbases db)
+  | TacAuto (n,db) ->
+      hov 0 (str "Auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
   | TacAutoTDB None as x -> pr_atom0 x
   | TacAutoTDB (Some n) -> hov 0 (str "AutoTDB" ++ spc () ++ int n)
   | TacDestructHyp (true,(_,id)) -> hov 0 (str "CDHyp" ++ spc () ++ pr_id id)
@@ -544,7 +545,7 @@ and pr_atom1 = function
       hov 1 (str "SuperAuto" ++ pr_opt int n ++ pr_autoarg_adding l ++ 
              pr_autoarg_destructing b1 ++ pr_autoarg_usingTDB b2)
   | TacDAuto (n,p) ->
-      hov 1 (str "Auto" ++ pr_opt int n ++ str "Decomp" ++ pr_opt int p)
+      hov 1 (str "Auto" ++ pr_opt (pr_or_var int) n ++ str "Decomp" ++ pr_opt int p)
 
   (* Context management *)
   | TacClear (keep,l) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index a411d0ddde..d963d94509 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -464,7 +464,7 @@ let rec mlexpr_of_atomic_tactic = function
 
   (* Automation tactics *)
   | Tacexpr.TacAuto (n,l) ->
-      let n = mlexpr_of_option mlexpr_of_int n in
+      let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
       <:expr< Tacexpr.TacAuto $n$ $l$ >>
 (*