Adding a test for #6304 (bug with fix in notations).

2 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 1ec701ae8..f57cc163d 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -84,3 +84,9 @@ a≡
      : Set
 .α
      : Set
+# a : .α =>
+# b : .α =>
+let res := 0 in
+for i from 0 to a updating (res)
+{{for j from 0 to b updating (res) {{S res}};; res}};; res
+     : .α -> .α -> .α
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index ceb29d1b9..9ca180c9d 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -145,3 +145,24 @@ Check .a≡.
 Notation ".α" := nat.
 Check nat.
 Check .α.
+
+(* A test for #6304 *)
+
+Module M6304.
+Notation "'for' m 'from' 0 'to' N 'updating' ( s1 )  {{ b }} ;; rest" :=
+  (let s1 :=
+    (fix rec(n: nat) := match n with
+     | 0 => s1
+     | S m => let s1 := rec m in b
+     end) N
+  in rest)
+  (at level 20).
+
+Check fun (a b : nat) =>
+  let res := 0 in
+  for i from 0 to a updating (res) {{
+    for j from 0 to b updating (res) {{ S res }};;
+    res
+  }};; res.
+
+End M6304.