Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.

Reviewed-by: JasonGross
Ack-by: jfehrle

4 files changed, 65 insertions, 5 deletions

diff --git a/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
new file mode 100644
index 0000000000..41bc3329c1
--- /dev/null
+++ b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Ltac2 notations now correctly take into account their assigned level
+  (`#14094 <https://github.com/coq/coq/pull/14094>`_,
+  fixes `#11866 <https://github.com/coq/coq/issues/11866>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 25ac72069b..52cf565998 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1251,6 +1251,10 @@ Notations
 
    This command supports the :attr:`deprecated` attribute.
 
+   .. exn:: Notation levels must range between 0 and 6.
+
+      The level of a notation must be an integer between 0 and 6 inclusive.
+
 Abbreviations
 ~~~~~~~~~~~~~
 
diff --git a/test-suite/bugs/closed/bug_11866.v b/test-suite/bugs/closed/bug_11866.v
new file mode 100644
index 0000000000..5a47f3833e
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11866.v
@@ -0,0 +1,43 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Notation "ex0" x(tactic(0)) := ().
+Ltac2 Notation "ex1" x(tactic(1)) := ().
+Ltac2 Notation "ex2" x(tactic(2)) := ().
+Ltac2 Notation "ex3" x(tactic(3)) := ().
+Ltac2 Notation "ex4" x(tactic(4)) := ().
+Ltac2 Notation "ex5" x(tactic(5)) := ().
+Ltac2 Notation "ex6" x(tactic(6)) := ().
+
+Ltac2 Notation ":::0" x(tactic) "+0" y(tactic) : 0 := ().
+Ltac2 Notation ":::1" x(tactic) "+1" y(tactic) : 1 := ().
+Ltac2 Notation ":::2" x(tactic) "+2" y(tactic) : 2 := ().
+Ltac2 Notation ":::3" x(tactic) "+3" y(tactic) : 3 := ().
+Ltac2 Notation ":::4" x(tactic) "+4" y(tactic) : 4 := ().
+Ltac2 Notation ":::5" x(tactic) "+5" y(tactic) : 5 := ().
+Ltac2 Notation ":::6" x(tactic) "+6" y(tactic) : 6 := ().
+Fail Ltac2 Notation ":::7" x(tactic) "+7" y(tactic) : 7 := ().
+Goal True.
+  ex0 :::0 0 +0 0.
+  ex1 :::0 0 +0 0.
+  (*ex2 :::0 0 +0 0.*) (* fails with an anomaly, cf COQBUG(https://github.com/coq/coq/issues/12807) *)
+  (*ex3 :::0 0 +0 0.*)
+  ex4 :::0 0 +0 0.
+  ex5 :::0 0 +0 0.
+  ex6 :::0 0 +0 0.
+
+  ex0 :::1 0 +1 0.
+  ex1 :::1 0 +1 0.
+  (*ex2 :::1 0 +1 0.*)
+  (*ex3 :::1 0 +1 0.*)
+  ex4 :::1 0 +1 0.
+  ex5 :::1 0 +1 0.
+  ex6 :::1 0 +1 0.
+
+  ex0 :::6 0 +6 0.
+  ex1 :::6 0 +6 0.
+  (*ex2 :::6 0 +6 0.*)
+  (*ex3 :::6 0 +6 0.*)
+  ex4 :::6 0 +6 0.
+  ex5 :::6 0 +6 0.
+  ex6 :::6 0 +6 0.
+Abort.
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 7af530ab0f..6aa31e9c91 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -675,12 +675,12 @@ let perform_notation syn st =
     CAst.make ~loc @@ CTacLet (false, bnd, syn.synext_exp)
   in
   let rule = Pcoq.Production.make rule (act mk) in
-  let lev = match syn.synext_lev with
+  let pos = match syn.synext_lev with
   | None -> None
-  | Some lev -> Some (string_of_int lev)
+  | Some lev -> Some (Gramlib.Gramext.Level (string_of_int lev))
   in
-  let rule = (lev, None, [rule]) in
-  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos=None; data=[rule]})], st)
+  let rule = (None, None, [rule]) in
+  ([Pcoq.ExtendRule (Pltac.ltac2_expr, {Pcoq.pos; data=[rule]})], st)
 
 let ltac2_notation =
   Pcoq.create_grammar_command "ltac2-notation" perform_notation
@@ -754,7 +754,15 @@ let register_notation ?deprecation ?(local = false) tkn lev body = match tkn, le
   let ids = List.fold_left fold Id.Set.empty entries in
   (* Globalize so that names are absolute *)
   let body = Tac2intern.globalize ids body in
-  let lev = match lev with Some _ -> lev | None -> Some 5 in
+  let lev = match lev with
+  | Some n ->
+    let () =
+      if n < 0 || n > 6 then
+        user_err (str "Notation levels must range between 0 and 6")
+    in
+    lev
+  | None -> Some 5
+  in
   let ext = {
     synext_tok = tkn;
     synext_exp = body;