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

8 files changed, 23 insertions, 17 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$ >>
 (*
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 3d060a8a3f..7ee45f67de 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -148,12 +148,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
 
   (* Automation tactics *)
   | TacTrivial of string list option
-  | TacAuto of int option * string list option
+  | TacAuto of int or_var option * string list option
   | TacAutoTDB of int option
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
   | TacSuperAuto of (int option * reference list * bool * bool)
-  | TacDAuto of int option * int option
+  | TacDAuto of int or_var option * int option
 
   (* Context management *)
   | TacClear of bool * 'id list
diff --git a/tactics/auto.ml b/tactics/auto.ml
index c30c0bd9f7..ea7c62a1c3 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -828,7 +828,10 @@ let gen_auto n dbnames =
   | None -> full_auto n
   | Some l -> auto n l
 
-let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l)
+let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+
+let h_auto n l =
+  Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l)
 
 (**************************************************************************)
 (*                  The "destructing Auto" from Eduardo                   *)
@@ -855,7 +858,8 @@ let dauto = function
   | Some n, Some p -> dautomatic p n
   | None, Some p   -> dautomatic p !default_search_depth
 
-let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p))
+let h_dauto (n,p) =
+  Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p))
 
 (***************************************)
 (*** A new formulation of Auto *********)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e284554e7c..76b99925ac 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -692,12 +692,12 @@ let rec intern_atomic lf ist x =
 
   (* Automation tactics *)
   | TacTrivial l -> TacTrivial l
-  | TacAuto (n,l) -> TacAuto (n,l)
+  | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
   | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
-  | TacDAuto (n,p) -> TacDAuto (n,p)
+  | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction (h,ids) ->
@@ -1716,12 +1716,12 @@ and interp_atomic ist gl = function
 *)
   (* Automation tactics *)
   | TacTrivial l -> Auto.h_trivial l
-  | TacAuto (n, l) -> Auto.h_auto n l
+  | TacAuto (n, l) -> Auto.h_auto (option_app (interp_int_or_var ist) n) l
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
   | TacDestructConcl -> Dhyp.h_destructConcl
   | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
-  | TacDAuto (n,p) -> Auto.h_dauto (n,p)
+  | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
 
   (* Derived basic tactics *)
   | TacSimpleInduction (h,ids) ->
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 29203afd0b..141ae1cbe6 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -595,7 +595,8 @@ and pr_atom1 env = function
   | TacTrivial (Some []) as x -> pr_atom0 env x
   | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db)
   | TacAuto (None,Some []) as x -> pr_atom0 env 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 env x
   | TacAutoTDB (Some n) -> hov 0 (str "autotdb" ++ spc () ++ int n)
   | TacDestructHyp (true,id) ->
@@ -607,7 +608,7 @@ and pr_atom1 env = 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) ->