1 files changed, 30 insertions, 0 deletions
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.