From da28b6e65d9b9a74c277cb15055131c8a151bb72 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 5 Sep 2017 00:42:22 +0200
Subject: Quotations for auto-related tactics.

---
 src/g_ltac2.ml4 | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'src/g_ltac2.ml4')

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)
-- 
cgit v1.2.3