8 files changed, 188 insertions, 5 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6696f1431e..0d8a6ebed7 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -417,14 +417,16 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
 	  output=$*.out.real; \
+	  export LC_CTYPE=C; \
+	  export LANG=C; \
 	  $(coqc_interactive) "$<" $(call get_coq_prog_args,"$<") 2>&1 \
-	    | grep -v "Welcome to Coq" \
-	    | grep -v "\[Loading ML file" \
-	    | grep -v "Skipping rcfile loading" \
-	    | grep -v "^<W>" \
+	    | grep -a -v "Welcome to Coq" \
+	    | grep -a -v "\[Loading ML file" \
+	    | grep -a -v "Skipping rcfile loading" \
+	    | grep -a -v "^<W>" \
 	    | sed 's/File "[^"]*"/File "stdin"/' \
 	    > $$output; \
-	  diff -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
+	  diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \
 	  if [ $$R = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/bugs/closed/bug_11890.v b/test-suite/bugs/closed/bug_11890.v
new file mode 100644
index 0000000000..c0426fcfda
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11890.v
@@ -0,0 +1,10 @@
+Require Import Coq.Structures.Orders Coq.ZArith.ZArith Coq.Sorting.Mergesort.
+(* Note that this has always worked fine without the '; we are testing importing notations from the stdlib here *)
+Declare Module A : LeBool'.
+Declare Module B : LtBool'.
+Import A B NatOrder.
+(*
+Error: Notation "_ <=? _" is already defined at level 70 with arguments constr
+at next level, constr at next level while it is now required to be at level 35
+with arguments constr at next level, constr at next level.
+*)
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 113384e9cf..060877707b 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -218,3 +218,19 @@ let v : ty := Build_ty Set set in v : ty
      : ty
 let v : ty := Build_ty Type type in v : ty
      : ty
+1
+     : nat
+(-1000)%Z
+     : Z
+0
+     : Prop
++0
+     : bool
+-0
+     : bool
+00
+     : nat * nat
+1000
+     : Prop
+1_000
+     : list nat
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 22aff36d67..47e1b127cb 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -457,3 +457,33 @@ Module Test20.
   Check let v := 4%kt in v : ty.
   Check let v := 5%kt in v : ty.
 End Test20.
+
+Module Test21.
+
+  Check 00001.
+  Check (-1_000)%Z.
+
+End Test21.
+
+Module Test22.
+
+Notation "0" := False.
+Notation "+0" := true.
+Notation "-0" := false.
+Notation "00" := (0%nat, 0%nat).
+Check 0.
+Check +0.
+Check -0.
+Check 00.
+
+Notation "1000" := True.
+Notation "1_000" := (cons 1 nil).
+Check 1000.
+Check 1_000.
+
+(* To do: preserve parsing of -0:
+Require Import ZArith.
+Check (-0)%Z.
+*)
+
+End Test22.
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out
index 2b14ca7069..ebc272d9af 100644
--- a/test-suite/output/RealSyntax.out
+++ b/test-suite/output/RealSyntax.out
@@ -4,6 +4,8 @@
      : R
 15e-1%R
      : R
+15%R
+     : R
 eq_refl : 102e-2 = 102e-2
      : 102e-2 = 102e-2
 eq_refl : 102e-1 = 102e-1
diff --git a/test-suite/output/RealSyntax.v b/test-suite/output/RealSyntax.v
index 7be8b18ac8..e5f9d06316 100644
--- a/test-suite/output/RealSyntax.v
+++ b/test-suite/output/RealSyntax.v
@@ -3,6 +3,7 @@ Check 32%R.
 Check (-31)%R.
 
 Check 1.5_%R.
+Check 1_.5_e1_%R.
 
 Open Scope R_scope.
 
diff --git a/test-suite/output/allBytes.out b/test-suite/output/allBytes.out
new file mode 100644
index 0000000000..8d188c4c45
--- /dev/null
+++ b/test-suite/output/allBytes.out
@@ -0,0 +1 @@
+!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~
diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v
new file mode 100644
index 0000000000..01a5161ef4
--- /dev/null
+++ b/test-suite/output/allBytes.v
@@ -0,0 +1,121 @@
+(* Taken from bedrock2 *)
+
+(* Note: not an utf8 file *)
+
+Require Import Coq.ZArith.BinInt Coq.Lists.List.
+Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String.
+
+Definition allBytes: list Byte.byte :=
+  map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with
+                 | Some b => b
+                 | None => Byte.x00 (* won't happen *)
+                 end)
+      (seq 32 95).
+
+Notation "a b" := (@cons Byte.byte a b)
+  (only printing, right associativity, at level 3, format "a b").
+
+Notation "" := (@nil Byte.byte)
+  (only printing, right associativity, at level 3, format "").
+
+Notation "  " := (Byte.x20) (only printing).
+Notation "'!'" := (Byte.x21) (only printing).
+Notation "'""'" := (Byte.x22) (only printing).
+Notation "'#'" := (Byte.x23) (only printing).
+Notation "'$'" := (Byte.x24) (only printing).
+Notation "'%'" := (Byte.x25) (only printing).
+Notation "'&'" := (Byte.x26) (only printing).
+Notation "'''" := (Byte.x27) (only printing).
+Notation "'('" := (Byte.x28) (only printing).
+Notation "')'" := (Byte.x29) (only printing).
+Notation "'*'" := (Byte.x2a) (only printing).
+Notation "'+'" := (Byte.x2b) (only printing).
+Notation "','" := (Byte.x2c) (only printing).
+Notation "'-'" := (Byte.x2d) (only printing).
+Notation "'.'" := (Byte.x2e) (only printing).
+Notation "'/'" := (Byte.x2f) (only printing).
+Notation "'0'" := (Byte.x30) (only printing).
+Notation "'1'" := (Byte.x31) (only printing).
+Notation "'2'" := (Byte.x32) (only printing).
+Notation "'3'" := (Byte.x33) (only printing).
+Notation "'4'" := (Byte.x34) (only printing).
+Notation "'5'" := (Byte.x35) (only printing).
+Notation "'6'" := (Byte.x36) (only printing).
+Notation "'7'" := (Byte.x37) (only printing).
+Notation "'8'" := (Byte.x38) (only printing).
+Notation "'9'" := (Byte.x39) (only printing).
+Notation "':'" := (Byte.x3a) (only printing).
+Notation "';'" := (Byte.x3b) (only printing).
+Notation "'<'" := (Byte.x3c) (only printing).
+Notation "'='" := (Byte.x3d) (only printing).
+Notation "'>'" := (Byte.x3e) (only printing).
+Notation "'?'" := (Byte.x3f) (only printing).
+Notation "'@'" := (Byte.x40) (only printing).
+Notation "'A'" := (Byte.x41) (only printing).
+Notation "'B'" := (Byte.x42) (only printing).
+Notation "'C'" := (Byte.x43) (only printing).
+Notation "'D'" := (Byte.x44) (only printing).
+Notation "'E'" := (Byte.x45) (only printing).
+Notation "'F'" := (Byte.x46) (only printing).
+Notation "'G'" := (Byte.x47) (only printing).
+Notation "'H'" := (Byte.x48) (only printing).
+Notation "'I'" := (Byte.x49) (only printing).
+Notation "'J'" := (Byte.x4a) (only printing).
+Notation "'K'" := (Byte.x4b) (only printing).
+Notation "'L'" := (Byte.x4c) (only printing).
+Notation "'M'" := (Byte.x4d) (only printing).
+Notation "'N'" := (Byte.x4e) (only printing).
+Notation "'O'" := (Byte.x4f) (only printing).
+Notation "'P'" := (Byte.x50) (only printing).
+Notation "'Q'" := (Byte.x51) (only printing).
+Notation "'R'" := (Byte.x52) (only printing).
+Notation "'S'" := (Byte.x53) (only printing).
+Notation "'T'" := (Byte.x54) (only printing).
+Notation "'U'" := (Byte.x55) (only printing).
+Notation "'V'" := (Byte.x56) (only printing).
+Notation "'W'" := (Byte.x57) (only printing).
+Notation "'X'" := (Byte.x58) (only printing).
+Notation "'Y'" := (Byte.x59) (only printing).
+Notation "'Z'" := (Byte.x5a) (only printing).
+Notation "'['" := (Byte.x5b) (only printing).
+Notation "'\'" := (Byte.x5c) (only printing).
+Notation "']'" := (Byte.x5d) (only printing).
+Notation "'^'" := (Byte.x5e) (only printing).
+Notation "'_'" := (Byte.x5f) (only printing).
+Notation "'`'" := (Byte.x60) (only printing).
+Notation "'a'" := (Byte.x61) (only printing).
+Notation "'b'" := (Byte.x62) (only printing).
+Notation "'c'" := (Byte.x63) (only printing).
+Notation "'d'" := (Byte.x64) (only printing).
+Notation "'e'" := (Byte.x65) (only printing).
+Notation "'f'" := (Byte.x66) (only printing).
+Notation "'g'" := (Byte.x67) (only printing).
+Notation "'h'" := (Byte.x68) (only printing).
+Notation "'i'" := (Byte.x69) (only printing).
+Notation "'j'" := (Byte.x6a) (only printing).
+Notation "'k'" := (Byte.x6b) (only printing).
+Notation "'l'" := (Byte.x6c) (only printing).
+Notation "'m'" := (Byte.x6d) (only printing).
+Notation "'n'" := (Byte.x6e) (only printing).
+Notation "'o'" := (Byte.x6f) (only printing).
+Notation "'p'" := (Byte.x70) (only printing).
+Notation "'q'" := (Byte.x71) (only printing).
+Notation "'r'" := (Byte.x72) (only printing).
+Notation "'s'" := (Byte.x73) (only printing).
+Notation "'t'" := (Byte.x74) (only printing).
+Notation "'u'" := (Byte.x75) (only printing).
+Notation "'v'" := (Byte.x76) (only printing).
+Notation "'w'" := (Byte.x77) (only printing).
+Notation "'x'" := (Byte.x78) (only printing).
+Notation "'y'" := (Byte.x79) (only printing).
+Notation "'z'" := (Byte.x7a) (only printing).
+Notation "'{'" := (Byte.x7b) (only printing).
+Notation "'|'" := (Byte.x7c) (only printing).
+Notation "'}'" := (Byte.x7d) (only printing).
+Notation "'~'" := (Byte.x7e) (only printing).
+
+Global Set Printing Width 300.
+
+Goal False.
+  let cc := eval cbv in allBytes in idtac cc.
+Abort.