Fix conflicts with latest master.

9 files changed, 43 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 ']' ']'"
+    ).
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index f48eaac4c9..9cb019ca56 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -111,3 +111,11 @@ Warning: The format modifier is irrelevant for only parsing rules.
 File "stdin", line 280, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
+fun x : nat => U (S x)
+     : nat -> nat
+V tt
+     : unit * (unit -> unit)
+fun x : nat => V x
+     : forall x : nat, nat * (?T -> ?T)
+where
+?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4d4b37a8b2..b3270d4f92 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -280,3 +280,13 @@ Notation "###" := 0 (at level 0, only parsing, format "###").
 Reserved Notation "##" (at level 0, only parsing, format "##").
 
 End N.
+
+Module O.
+
+Notation U t := (match t with 0 => 0 | S t => t | _ => 0 end).
+Check fun x => U (S x).
+Notation V t := (t,fun t => t).
+Check V tt.
+Check fun x : nat => V x.
+
+End O.
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out
new file mode 100644
index 0000000000..68dbaeb7b3
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.out
@@ -0,0 +1,4 @@
+While loading initial state:
+Warning: There is no flag or option with this name: "Extraction Optimize".
+[unknown-option,option]
+Extraction Optimize is on
diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v
new file mode 100644
index 0000000000..9a70674b02
--- /dev/null
+++ b/test-suite/output/interleave_options_bad_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *)
+
+Test Extraction Optimize.
diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out
new file mode 100644
index 0000000000..76bb2016eb
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.out
@@ -0,0 +1 @@
+Extraction Optimize is off
diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v
new file mode 100644
index 0000000000..7622d6ff52
--- /dev/null
+++ b/test-suite/output/interleave_options_correct_order.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *)
+
+Test Extraction Optimize.