Quotations for auto-related tactics.

7 files changed, 25 insertions, 1 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