diff options
Diffstat (limited to 'src/g_ltac2.ml4')
| -rw-r--r-- | src/g_ltac2.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index c1025ceba5..95fcf79000 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -327,7 +327,7 @@ open Tac2entries.Pltac 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 + GLOBAL: q_ident q_with_bindings q_intropattern q_intropatterns q_induction_clause q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag q_reference; anti: @@ -365,7 +365,7 @@ GEXTEND Gram Loc.tag ~loc:!@loc @@ QImplicitBindings bl ] ] ; - q_bindings: + q_with_bindings: [ [ bl = with_bindings -> bl ] ] ; intropatterns: |