diff options
| author | Pierre-Marie Pédrot | 2017-09-05 00:42:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:06:23 +0200 |
| commit | da28b6e65d9b9a74c277cb15055131c8a151bb72 (patch) | |
| tree | 38697f7a7ddebd9006bae72405131fe906c83a85 /src/g_ltac2.ml4 | |
| parent | ebe95a28cf012aff33eb5ce167be6520e6643cfd (diff) | |
Quotations for auto-related tactics.
Diffstat (limited to 'src/g_ltac2.ml4')
| -rw-r--r-- | src/g_ltac2.ml4 | 11 |
1 files changed, 10 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) |