diff options
| author | herbelin | 2005-05-15 12:48:57 +0000 |
|---|---|---|
| committer | herbelin | 2005-05-15 12:48:57 +0000 |
| commit | 1e095dd3f8b61a50dfd19f72d12e37a26a64435a (patch) | |
| tree | df1e72d2b287273edbdadd3669c1c9c1c07b0553 /tactics/auto.ml | |
| parent | b7c470ca84259c39df9491a25aadb0debe428b7c (diff) | |
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
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 6 insertions, 2 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 *********) |