aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/g_ltac2.ml411
-rw-r--r--src/tac2core.ml1
-rw-r--r--src/tac2entries.ml1
-rw-r--r--src/tac2entries.mli1
-rw-r--r--src/tac2qexpr.mli6
-rw-r--r--src/tac2quote.ml4
-rw-r--r--src/tac2quote.mli2
-rw-r--r--theories/Notations.v66
-rw-r--r--theories/Std.v2
9 files changed, 92 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index be7f830605..67254d0781 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -368,7 +368,8 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
GEXTEND Gram
GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag
- q_destruction_arg q_reference q_with_bindings q_constr_matching;
+ q_destruction_arg q_reference q_with_bindings q_constr_matching
+ q_hintdb;
anti:
[ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
;
@@ -664,6 +665,14 @@ GEXTEND Gram
q_strategy_flag:
[ [ flag = strategy_flag -> flag ] ]
;
+ hintdb:
+ [ [ "*" -> Loc.tag ~loc:!@loc @@ QHintAll
+ | l = LIST1 ident_or_anti -> Loc.tag ~loc:!@loc @@ QHintDbs l
+ ] ]
+ ;
+ q_hintdb:
+ [ [ db = hintdb -> db ] ]
+ ;
match_pattern:
[ [ IDENT "context"; id = OPT Prim.ident;
"["; pat = Constr.lconstr_pattern; "]" -> (Some id, pat)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 867c9ae806..a735dd19d9 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -1137,6 +1137,7 @@ let () = add_expr_scope "destruction_arg" q_destruction_arg Tac2quote.of_destruc
let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause
let () = add_expr_scope "rewriting" q_rewriting Tac2quote.of_rewriting
let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
+let () = add_expr_scope "hintdb" q_hintdb Tac2quote.of_hintdb
let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index afbbcfc15e..121841e8dc 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -38,6 +38,7 @@ let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
let q_reference = Pcoq.Gram.entry_create "tactic:q_reference"
let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
let q_constr_matching = Pcoq.Gram.entry_create "tactic:q_constr_matching"
+let q_hintdb = Pcoq.Gram.entry_create "tactic:q_hintdb"
end
(** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 581d04d8cc..91e2a683d8 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -73,6 +73,7 @@ val q_occurrences : occurrences Pcoq.Gram.entry
val q_reference : Libnames.reference or_anti Pcoq.Gram.entry
val q_strategy_flag : strategy_flag Pcoq.Gram.entry
val q_constr_matching : constr_matching Pcoq.Gram.entry
+val q_hintdb : hintdb Pcoq.Gram.entry
end
(** {5 Hooks} *)
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 577fe8edfe..4bbaf43d8d 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -125,3 +125,9 @@ type constr_match_branch_r =
type constr_match_branch = constr_match_branch_r located
type constr_matching = constr_match_branch list located
+
+type hintdb_r =
+| QHintAll
+| QHintDbs of Id.t located or_anti list
+
+type hintdb = hintdb_r located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index ed4cef2e2a..f87985435c 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -305,6 +305,10 @@ let of_strategy_flag (loc, flag) =
std_proj "rConst", of_list ?loc of_reference flag.rConst;
])
+let of_hintdb (loc, hdb) = match hdb with
+| QHintAll -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) None
+| QHintDbs ids -> of_option ?loc (fun l -> of_list (fun id -> of_anti of_ident id) l) (Some ids)
+
let pattern_vars pat =
let rec aux () accu pat = match pat.CAst.v with
| Constrexpr.CPatVar id -> Id.Set.add id accu
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 875230b7e3..b85f3438a3 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -54,6 +54,8 @@ val of_rewriting : rewriting -> raw_tacexpr
val of_occurrences : occurrences -> raw_tacexpr
+val of_hintdb : hintdb -> raw_tacexpr
+
val of_reference : Libnames.reference or_anti -> raw_tacexpr
val of_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
diff --git a/theories/Notations.v b/theories/Notations.v
index 136ca871c2..4cb4f32682 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -432,6 +432,72 @@ Ltac2 Notation "injection" arg(opt(destruction_arg)) ipat(opt(seq("as", intropat
Ltac2 Notation "einjection" arg(opt(destruction_arg)) ipat(opt(seq("as", intropatterns))):=
Std.injection true ipat arg.
+(** Auto *)
+
+Ltac2 default_db dbs := match dbs with
+| None => Some []
+| Some dbs =>
+ match dbs with
+ | None => None
+ | Some l => Some l
+ end
+end.
+
+Ltac2 default_using use := match use with
+| None => []
+| Some use => use
+end.
+
+Ltac2 trivial0 use dbs :=
+ let dbs := default_db dbs in
+ let use := default_using use in
+ Std.trivial Std.Off use dbs.
+
+Ltac2 Notation "trivial"
+ use(opt(seq("using", list1(thunk(constr), ","))))
+ dbs(opt(seq("with", hintdb))) := trivial0 use dbs.
+
+Ltac2 Notation trivial := trivial.
+
+Ltac2 auto0 n use dbs :=
+ let dbs := default_db dbs in
+ let use := default_using use in
+ Std.auto Std.Off n use dbs.
+
+Ltac2 Notation "auto" n(opt(tactic(0)))
+ use(opt(seq("using", list1(thunk(constr), ","))))
+ dbs(opt(seq("with", hintdb))) := auto0 n use dbs.
+
+Ltac2 Notation auto := auto.
+
+Ltac2 new_eauto0 n use dbs :=
+ let dbs := default_db dbs in
+ let use := default_using use in
+ Std.new_auto Std.Off n use dbs.
+
+Ltac2 Notation "new" "auto" n(opt(tactic(0)))
+ use(opt(seq("using", list1(thunk(constr), ","))))
+ dbs(opt(seq("with", hintdb))) := new_eauto0 n use dbs.
+
+Ltac2 eauto0 n p use dbs :=
+ let dbs := default_db dbs in
+ let use := default_using use in
+ Std.eauto Std.Off n p use dbs.
+
+Ltac2 Notation "eauto" n(opt(tactic(0))) p(opt(tactic(0)))
+ use(opt(seq("using", list1(thunk(constr), ","))))
+ dbs(opt(seq("with", hintdb))) := eauto0 n p use dbs.
+
+Ltac2 Notation eauto := eauto.
+
+Ltac2 Notation "typeclasses_eauto" n(opt(tactic(0))) p(opt(tactic(0)))
+ dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.DFS n dbs.
+
+Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) p(opt(tactic(0)))
+ dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.BFS n dbs.
+
+Ltac2 Notation typeclasses_eauto := typeclasses_eauto.
+
(** Congruence *)
Ltac2 f_equal0 () := ltac1:(f_equal).
diff --git a/theories/Std.v b/theories/Std.v
index 5201fa819d..79a7be1d63 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -216,7 +216,7 @@ Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".
Ltac2 Type debug := [ Off | Info | Debug ].
-Ltac2 Type strategy := [ BFS | DFS ].
+Ltac2 Type strategy := [ BFS | DFS ].
Ltac2 @ external trivial : debug -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_trivial".
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 13:08:10 +0000