From 8e6338d862873d7e377f59664bbd89e16c0a7309 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Aug 2017 18:03:54 +0200
Subject: Introducing a distinct bindings scope.

---
 src/g_ltac2.ml4     | 7 +++++--
 src/tac2core.ml     | 1 +
 src/tac2entries.ml  | 1 +
 src/tac2entries.mli | 1 +
 4 files changed, 8 insertions(+), 2 deletions(-)

(limited to 'src')

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