Fix conflicts with latest master.

3 files changed, 14 insertions, 1 deletions

diff --git a/test-suite/bugs/closed/bug_7903.v b/test-suite/bugs/closed/bug_7903.v
index 55c7ee99a7..18e1884ca7 100644
--- a/test-suite/bugs/closed/bug_7903.v
+++ b/test-suite/bugs/closed/bug_7903.v
@@ -1,4 +1,4 @@
 (* Slightly improving interpretation of Ltac subterms in notations *)
 
 Notation bar x f := (let z := ltac:(exact 1) in (fun x : nat => f)).
-Check bar x (x + x).
+Check fun x => bar x (x + x).
diff --git a/test-suite/bugs/closed/bug_9583.v b/test-suite/bugs/closed/bug_9583.v
new file mode 100644
index 0000000000..14232e8578
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9583.v
@@ -0,0 +1,7 @@
+(* Was causing a stack overflow before #11613 *)
+Declare Custom Entry bla.
+Notation "[ t ]" := (t) (at level 0, t custom bla at level 0).
+Notation "] t [" := (t) (in custom bla at level 0, t custom bla at level 0).
+Notation "t" := (t) (in custom bla at level 0, t constr at level 9).
+Notation "0" := (0) (in custom bla at level 0).
+Check fun x => [ ] x [ ].
diff --git a/test-suite/bugs/closed/bug_9679.v b/test-suite/bugs/closed/bug_9679.v
new file mode 100644
index 0000000000..24e69d23f9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9679.v
@@ -0,0 +1,6 @@
+(* Was raising an anomaly *)
+Notation "'[#' ] f '|' x .. z '=n>' b" :=
+  (fun x => .. (fun z => f b) ..)
+    (at level 201, x binder, z binder,
+     format "'[  ' [# ] '[' f  | ']'  x  ..  z  =n>  '[' b ']' ']'"
+    ).