Renaming the bindings scope into with_bindings.

5 files changed, 25 insertions, 25 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:
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 7a8f3ceb44..342e8f51e8 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -912,7 +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
 let () = add_expr_scope "induction_clause" q_induction_clause Tac2quote.of_induction_clause
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 73086c406e..6c8c2348fe 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -25,7 +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"
 let q_induction_clause = Pcoq.Gram.entry_create "tactic:q_induction_clause"
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 8b92bd16f6..d22ae7a953 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -60,7 +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
 val q_induction_clause : induction_clause Pcoq.Gram.entry
diff --git a/theories/Notations.v b/theories/Notations.v
index bb27a34627..8345344d94 100644
--- a/theories/Notations.v
+++ b/theories/Notations.v
@@ -124,10 +124,10 @@ Ltac2 Notation eintros := eintros.
 Ltac2 split0 ev bnd :=
   enter_h ev Std.split bnd.
 
-Ltac2 Notation "split" bnd(thunk(bindings)) := split0 false bnd.
+Ltac2 Notation "split" bnd(thunk(with_bindings)) := split0 false bnd.
 Ltac2 Notation split := split.
 
-Ltac2 Notation "esplit" bnd(thunk(bindings)) := split0 true bnd.
+Ltac2 Notation "esplit" bnd(thunk(with_bindings)) := split0 true bnd.
 Ltac2 Notation esplit := esplit.
 
 Ltac2 exists0 ev bnds := match bnds with
@@ -141,26 +141,26 @@ Ltac2 exists0 ev bnds := match bnds with
 end.
 
 (*
-Ltac2 Notation "exists" bnd(list0(thunk(bindings), ",")) := exists0 false bnd.
+Ltac2 Notation "exists" bnd(list0(thunk(with_bindings), ",")) := exists0 false bnd.
 
-Ltac2 Notation "eexists" bnd(list0(thunk(bindings), ",")) := exists0 true bnd.
+Ltac2 Notation "eexists" bnd(list0(thunk(with_bindings), ",")) := exists0 true bnd.
 Ltac2 Notation eexists := eexists.
 *)
 
 Ltac2 left0 ev bnd := enter_h ev Std.left bnd.
 
-Ltac2 Notation "left" bnd(thunk(bindings)) := left0 false bnd.
+Ltac2 Notation "left" bnd(thunk(with_bindings)) := left0 false bnd.
 Ltac2 Notation left := left.
 
-Ltac2 Notation "eleft" bnd(thunk(bindings)) := left0 true bnd.
+Ltac2 Notation "eleft" bnd(thunk(with_bindings)) := left0 true bnd.
 Ltac2 Notation eleft := eleft.
 
 Ltac2 right0 ev bnd := enter_h ev Std.right bnd.
 
-Ltac2 Notation "right" bnd(thunk(bindings)) := right0 false bnd.
+Ltac2 Notation "right" bnd(thunk(with_bindings)) := right0 false bnd.
 Ltac2 Notation right := right.
 
-Ltac2 Notation "eright" bnd(thunk(bindings)) := right0 true bnd.
+Ltac2 Notation "eright" bnd(thunk(with_bindings)) := right0 true bnd.
 Ltac2 Notation eright := eright.
 
 Ltac2 constructor0 ev n bnd :=
@@ -168,22 +168,22 @@ Ltac2 constructor0 ev n bnd :=
 
 Ltac2 Notation "constructor" := Control.enter (fun () => Std.constructor false).
 Ltac2 Notation constructor := constructor.
-Ltac2 Notation "constructor" n(tactic) bnd(thunk(bindings)) := constructor0 false n bnd.
+Ltac2 Notation "constructor" n(tactic) bnd(thunk(with_bindings)) := constructor0 false n bnd.
 
 Ltac2 Notation "econstructor" := Control.enter (fun () => Std.constructor true).
 Ltac2 Notation econstructor := econstructor.
-Ltac2 Notation "econstructor" n(tactic) bnd(thunk(bindings)) := constructor0 true n bnd.
+Ltac2 Notation "econstructor" n(tactic) bnd(thunk(with_bindings)) := constructor0 true n bnd.
 
 Ltac2 elim0 ev c bnd use :=
   let f ev ((c, bnd, use)) := Std.elim ev (c, bnd) use in
   enter_h ev f (fun () => c (), bnd (), use ()).
 
-Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(bindings))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+Ltac2 Notation "elim" c(thunk(constr)) bnd(thunk(with_bindings))
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   elim0 false c bnd use.
 
-Ltac2 Notation "eelim" c(thunk(constr)) bnd(thunk(bindings))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+Ltac2 Notation "eelim" c(thunk(constr)) bnd(thunk(with_bindings))
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   elim0 true c bnd use.
 
 Ltac2 apply0 adv ev cb cl :=
@@ -202,12 +202,12 @@ Ltac2 apply0 adv ev cb cl :=
   Std.apply adv ev cb cl.
 
 Ltac2 Notation "eapply"
-  cb(list1(thunk(seq(constr, bindings)), ","))
+  cb(list1(thunk(seq(constr, with_bindings)), ","))
   cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
   apply0 true true cb cl.
 
 Ltac2 Notation "apply"
-  cb(list1(thunk(seq(constr, bindings)), ","))
+  cb(list1(thunk(seq(constr, with_bindings)), ","))
   cl(opt(seq(keyword("in"), ident, opt(seq(keyword("as"), intropattern))))) :=
   apply0 true false cb cl.
 
@@ -217,12 +217,12 @@ Ltac2 induction0 ev ic use :=
 
 Ltac2 Notation "induction"
   ic(list1(induction_clause, ","))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   induction0 false ic use.
 
 Ltac2 Notation "einduction"
   ic(list1(induction_clause, ","))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   induction0 true ic use.
 
 Ltac2 destruct0 ev ic use :=
@@ -231,12 +231,12 @@ Ltac2 destruct0 ev ic use :=
 
 Ltac2 Notation "destruct"
   ic(list1(induction_clause, ","))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   destruct0 false ic use.
 
 Ltac2 Notation "edestruct"
   ic(list1(induction_clause, ","))
-  use(thunk(opt(seq("using", constr, bindings)))) :=
+  use(thunk(opt(seq("using", constr, with_bindings)))) :=
   destruct0 true ic use.
 
 Ltac2 default_on_concl cl :=