diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 8 |
2 files changed, 10 insertions, 6 deletions
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) -> |