2 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index bb299eff97..060877707b 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -222,3 +222,15 @@ let v : ty := Build_ty Type type in v : ty
      : 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 31154d9f45..47e1b127cb 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -464,3 +464,26 @@ Module Test21.
   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.