Removing auto from the tactic AST.

8 files changed, 80 insertions, 84 deletions

diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 1b1fb845e..6a620deeb 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -221,8 +221,6 @@ let initial_atomic () =
         "intro", TacIntroMove(None,MoveLast);
         "intros", TacIntroPattern [];
         "cofix", TacCofix None;
-        "trivial", TacTrivial (Off,[],None);
-        "auto", TacAuto(Off,None,[],None);
       ]
   in
   let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ffde67e4f..1943a4f1f 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -438,37 +438,10 @@ let make_dimension n = function
   | Some d -> (false,d)
 
 open Genarg
+open G_auto
 
-(* Hint bases *)
-
-let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
-
-ARGUMENT EXTEND hintbases
-  TYPED AS preident_list_opt
-  PRINTED BY pr_hintbases
-| [ "with" "*" ] -> [ None ]
-| [ "with" ne_preident_list(l) ] -> [ Some l ]
-| [ ] -> [ Some [] ]
-END
-
-let pr_constr_coma_sequence prc _ _ =
-  prlist_with_sep pr_comma (fun (_,c) -> prc c)
-
-ARGUMENT EXTEND constr_coma_sequence
-  TYPED AS open_constr_list
-  PRINTED BY pr_constr_coma_sequence
-| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
-| [ open_constr(c) ] -> [ [c] ]
-END
-
-let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
-
-ARGUMENT EXTEND auto_using
-  TYPED AS open_constr_list
-  PRINTED BY pr_auto_using
-| [ "using" constr_coma_sequence(l) ] -> [ l ]
-| [ ] -> [ [] ]
-END
+let hintbases = G_auto.hintbases
+let wit_hintbases = G_auto.wit_hintbases
 
 TACTIC EXTEND eauto
 | [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems)
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index b55c70fa1..3d02081bf 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -15,12 +15,6 @@ val hintbases : hint_db_name list option Pcoq.Gram.entry
 
 val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type
 
-val wit_auto_using :
-  (Tacexpr.open_constr_expr list,
-  Tacexpr.open_glob_constr list, Evd.open_constr list)
-    Genarg.genarg_type
-
-
 val e_assumption : unit Proofview.tactic
 
 val registered_e_assumption : unit Proofview.tactic
diff --git a/tactics/g_auto.ml4 b/tactics/g_auto.ml4
new file mode 100644
index 000000000..7d35cfaab
--- /dev/null
+++ b/tactics/g_auto.ml4
@@ -0,0 +1,76 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "grammar/grammar.cma" i*)
+
+open Pp
+open Genarg
+open Tacexpr
+
+DECLARE PLUGIN "g_auto"
+
+(* Hint bases *)
+
+let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
+
+ARGUMENT EXTEND hintbases
+  TYPED AS preident_list_opt
+  PRINTED BY pr_hintbases
+| [ "with" "*" ] -> [ None ]
+| [ "with" ne_preident_list(l) ] -> [ Some l ]
+| [ ] -> [ Some [] ]
+END
+
+let pr_constr_coma_sequence prc _ _ =
+  prlist_with_sep pr_comma (fun (_,c) -> prc c)
+
+ARGUMENT EXTEND constr_coma_sequence
+  TYPED AS open_constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ open_constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
+| [ open_constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using (fun (_,c) -> prc c)
+
+ARGUMENT EXTEND auto_using
+  TYPED AS open_constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
+TACTIC EXTEND trivial
+| [ "trivial" auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_trivial lems db ]
+END
+
+TACTIC EXTEND info_trivial
+| [ "info_trivial" auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_trivial ~debug:Info lems db ]
+END
+
+TACTIC EXTEND debug_trivial
+| [ "debug" "trivial" auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_trivial ~debug:Debug lems db ]
+END
+
+TACTIC EXTEND auto
+| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_auto n lems db ]
+END
+
+TACTIC EXTEND info_auto
+| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_auto ~debug:Info n lems db ]
+END
+
+TACTIC EXTEND debug_auto
+| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] ->
+    [ Auto.h_auto ~debug:Debug n lems db ]
+END
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index ff2e1ff6a..30e97f62d 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,6 +1,7 @@
 Extraargs
 Coretactics
 Extratactics
+G_auto
 Eauto
 Class_tactics
 G_class
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 5e725e182..ecce4a0ff 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -517,12 +517,6 @@ let rec intern_atomic lf ist x =
                  (clause_app (intern_hyp_location ist) cls),b,
 		 (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
 
-  (* Automation tactics *)
-  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (intern_constr ist) lems,l)
-  | TacAuto (d,n,lems,l) ->
-      TacAuto (d,Option.map (intern_int_or_var ist) n,
-        List.map (intern_constr ist) lems,l)
-
   (* Derived basic tactics *)
   | TacInductionDestruct (ev,isrec,(l,el)) ->
       TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 570ab245b..8c8861fd9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1958,42 +1958,6 @@ and interp_atomic ist tac : unit Proofview.tactic =
                   ((sigma,sigma'),c) clp eqpat) sigma')
       end }
 
-  (* Automation tactics *)
-  | TacTrivial (debug,lems,l) ->
-      begin if debug == Tacexpr.Info then
-          msg_warning
-	    (strbrk"The \"info_trivial\" tactic" ++ spc ()
-           ++strbrk"does not print traces anymore." ++ spc()
-           ++strbrk"Use \"Info 1 trivial\", instead.")
-      end;
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Tacmach.New.project gl in
-        let lems = interp_auto_lemmas ist env sigma lems in
-        name_atomic ~env
-          (TacTrivial(debug,List.map snd lems,l))
-          (Auto.h_trivial ~debug
-	     lems
-	     (Option.map (List.map (interp_hint_base ist)) l))
-      end }
-  | TacAuto (debug,n,lems,l) ->
-      begin if debug == Tacexpr.Info then
-          msg_warning
-	    (strbrk"The \"info_auto\" tactic" ++ spc ()
-           ++strbrk"does not print traces anymore." ++ spc()
-           ++strbrk"Use \"Info 1 auto\", instead.")
-      end;
-      Proofview.Goal.enter { enter = begin fun gl ->
-        let env = Proofview.Goal.env gl in
-        let sigma = Tacmach.New.project gl in
-        let lems = interp_auto_lemmas ist env sigma lems in
-        name_atomic ~env
-          (TacAuto(debug,n,List.map snd lems,l))
-          (Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
-	     lems
-	     (Option.map (List.map (interp_hint_base ist)) l))
-      end }
-
   (* Derived basic tactics *)
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       (* spiwack: some unknown part of destruct needs the goal to be
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0c9665362..fdf65292a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -154,10 +154,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacLetTac (id,c,clp,b,eqpat) ->
     TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
 
-  (* Automation tactics *)
-  | TacTrivial (d,lems,l) -> TacTrivial (d,List.map (subst_glob_constr subst) lems,l)
-  | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l)
-
   (* Derived basic tactics *)
   | TacInductionDestruct (isrec,ev,(l,el)) ->
       let l' = List.map (fun (c,ids,cls) ->