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

2 files changed, 10 insertions, 6 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c30c0bd9f..ea7c62a1c 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 e284554e7..76b99925a 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) ->