aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml413
-rw-r--r--intf/tacexpr.mli4
-rw-r--r--parsing/g_tactic.ml414
-rw-r--r--plugins/firstorder/g_ground.ml49
-rw-r--r--printing/pptactic.ml19
-rw-r--r--tactics/coretactics.ml42
-rw-r--r--tactics/eauto.ml433
-rw-r--r--tactics/eauto.mli6
-rw-r--r--tactics/g_auto.ml476
-rw-r--r--tactics/hightactics.mllib1
-rw-r--r--tactics/tacintern.ml6
-rw-r--r--tactics/tacinterp.ml36
-rw-r--r--tactics/tacsubst.ml4
-rw-r--r--theories/Init/Notations.v1
14 files changed, 89 insertions, 135 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 7001f5f62..fc08f0a49 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -420,19 +420,6 @@ let rec mlexpr_of_atomic_tactic = function
(* Equivalence relations *)
| Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >>
- (* Automation tactics *)
- | Tacexpr.TacAuto (debug,n,lems,l) ->
- let d = mlexpr_of_debug debug in
- let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
- let lems = mlexpr_of_list mlexpr_of_constr lems in
- let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
- <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
- | Tacexpr.TacTrivial (debug,lems,l) ->
- let d = mlexpr_of_debug debug in
- let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
- let lems = mlexpr_of_list mlexpr_of_constr lems in
- <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
-
| _ -> failwith "Quotation of atomic tactic expressions: TODO"
and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index ead221c5f..aa1088c9e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -162,10 +162,6 @@ type 'a gen_atomic_tactic_expr =
rec_flag * evars_flag * ('trm,'dtrm,'nam) induction_clause_list
| TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
- (* Automation tactics *)
- | TacTrivial of debug * 'trm list * string list option
- | TacAuto of debug * int or_var option * 'trm list * string list option
-
(* Context management *)
| TacClear of bool * 'nam list
| TacClearBody of 'nam list
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 3e4a6c6a1..a197e0209 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -623,20 +623,6 @@ GEXTEND Gram
| IDENT "edestruct"; icl = induction_clause_list ->
TacAtom (!@loc, TacInductionDestruct(false,true,icl))
- (* Automation tactic *)
- | IDENT "trivial"; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacTrivial (Off, lems, db))
- | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacTrivial (Info, lems, db))
- | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacTrivial (Debug, lems, db))
- | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacAuto (Off, n, lems, db))
- | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacAuto (Info, n, lems, db))
- | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
- TacAtom (!@loc, TacAuto (Debug, n, lems, db))
-
(* Context management *)
| IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l))
| IDENT "clear"; l = LIST0 id_or_meta ->
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c28da42ae..9d853a79a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -52,8 +52,15 @@ let _=
in
declare_int_option gdopt
+let default_intuition_tac =
+ let tac _ _ = Auto.h_auto None [] None in
+ let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
+ let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
+ Tacenv.register_ml_tactic name [| tac |];
+ Tacexpr.TacML (Loc.ghost, entry, [])
+
let (set_default_solver, default_solver, print_default_solver) =
- Tactic_option.declare_tactic_option ~default:(<:tactic<auto with *>>) "Firstorder default solver"
+ Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
| [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 9c6da350f..ff83ac3e9 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -807,8 +807,6 @@ module Make
let rec pr_atom0 a = tag_atom a (match a with
| TacIntroPattern [] -> primitive "intros"
| TacIntroMove (None,MoveLast) -> primitive "intro"
- | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
- | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
| TacClear (true,[]) -> primitive "clear"
| t -> str "(" ++ pr_atom1 t ++ str ")"
)
@@ -917,23 +915,6 @@ module Make
++ pr_arg pr_quantified_hypothesis h2
)
- (* Automation tactics *)
- | TacTrivial (_,[],Some []) as x ->
- pr_atom0 x
- | TacTrivial (d,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "trivial"
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
- | TacAuto (_,None,[],Some []) as x ->
- pr_atom0 x
- | TacAuto (d,n,lems,db) ->
- hov 0 (
- str (string_of_debug d) ++ primitive "auto"
- ++ pr_opt (pr_or_var int) n
- ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
- )
-
(* Context management *)
| TacClear (true,[]) as t ->
pr_atom0 t
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) ->
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index a7bdba90a..2f6d824d2 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -85,6 +85,7 @@ Open Scope type_scope.
Declare ML Module "coretactics".
Declare ML Module "extratactics".
+Declare ML Module "g_auto".
Declare ML Module "eauto".
Declare ML Module "g_class".
Declare ML Module "g_eqdecide".
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 18:02:24 +0000