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

Reviewed-by: JasonGross
Ack-by: jfehrle

1 files changed, 43 insertions, 0 deletions

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.