diff options
| author | Pierre-Marie Pédrot | 2017-08-25 18:03:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-25 18:04:50 +0200 |
| commit | 8e6338d862873d7e377f59664bbd89e16c0a7309 (patch) | |
| tree | a878a65efc51382fbbf6047aa862e4cbb1386854 /src | |
| parent | 029dd0fcfc5641b689356c467e2f0fb1d3fa178c (diff) | |
Introducing a distinct bindings scope.
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 7 | ||||
| -rw-r--r-- | src/tac2core.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 |
4 files changed, 8 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 95fcf79000..e7ab574747 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -327,9 +327,9 @@ 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_with_bindings q_intropattern q_intropatterns q_induction_clause + GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag - q_reference; + q_reference q_with_bindings; anti: [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ] ; @@ -365,6 +365,9 @@ GEXTEND Gram Loc.tag ~loc:!@loc @@ QImplicitBindings bl ] ] ; + q_bindings: + [ [ bl = bindings -> bl ] ] + ; q_with_bindings: [ [ bl = with_bindings -> bl ] ] ; diff --git a/src/tac2core.ml b/src/tac2core.ml index 342e8f51e8..b67d70a5cb 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -912,6 +912,7 @@ let add_expr_scope name entry f = end let () = add_expr_scope "ident" q_ident (fun id -> Tac2quote.of_anti Tac2quote.of_ident id) +let () = add_expr_scope "bindings" q_bindings Tac2quote.of_bindings let () = add_expr_scope "with_bindings" q_with_bindings Tac2quote.of_bindings let () = add_expr_scope "intropattern" q_intropattern Tac2quote.of_intro_pattern let () = add_expr_scope "intropatterns" q_intropatterns Tac2quote.of_intro_patterns diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 6c8c2348fe..91c8d10e2d 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -25,6 +25,7 @@ struct let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr" let q_ident = Pcoq.Gram.entry_create "tactic:q_ident" +let q_bindings = Pcoq.Gram.entry_create "tactic:q_bindings" let q_with_bindings = Pcoq.Gram.entry_create "tactic:q_with_bindings" let q_intropattern = Pcoq.Gram.entry_create "tactic:q_intropattern" let q_intropatterns = Pcoq.Gram.entry_create "tactic:q_intropatterns" diff --git a/src/tac2entries.mli b/src/tac2entries.mli index d22ae7a953..2c5862b149 100644 --- a/src/tac2entries.mli +++ b/src/tac2entries.mli @@ -60,6 +60,7 @@ val tac2expr : raw_tacexpr Pcoq.Gram.entry open Tac2qexpr val q_ident : Id.t located or_anti Pcoq.Gram.entry +val q_bindings : bindings Pcoq.Gram.entry val q_with_bindings : bindings Pcoq.Gram.entry val q_intropattern : intro_pattern Pcoq.Gram.entry val q_intropatterns : intro_pattern list located Pcoq.Gram.entry |