1 files changed, 18 insertions, 0 deletions
diff --git a/src/Compilers/Z/BinaryNotationConstants.v b/src/Compilers/Z/BinaryNotationConstants.v
index 7c73cd8d2..375265c9c 100644
--- a/src/Compilers/Z/BinaryNotationConstants.v
+++ b/src/Compilers/Z/BinaryNotationConstants.v
@@ -79,6 +79,7 @@ nums = tuple(sorted(set(systematic_nums + [
     2095622,
     2096127,
     2096128,
+    2096583,
     2096942,
     2097098,
     2097114,
@@ -91,9 +92,11 @@ nums = tuple(sorted(set(systematic_nums + [
     4162878,
     4188670,
     4192254,
+    4193166,
     4193327,
     4193539,
     4193735,
+    4193823,
     4193883,
     4193987,
     4194115,
@@ -116,8 +119,10 @@ nums = tuple(sorted(set(systematic_nums + [
     8386654,
     8387078,
     8387470,
+    8387646,
     8387766,
     8387974,
+    8388127,
     8388187,
     8388230,
     8388291,
@@ -145,6 +150,7 @@ nums = tuple(sorted(set(systematic_nums + [
     16647166,
     16711679,
     16775935,
+    16776254,
     16776374,
     16776582,
     16776842,
@@ -1217,6 +1223,8 @@ Notation "'0b111111111101111111111'" (* 2096127 (0x1ffbff) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111110000000000'" (* 2096128 (0x1ffc00) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~0~0~0~0~0~0).
+Notation "'0b111111111110111000111'" (* 2096583 (0x1ffdc7) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1).
 Notation "'0b111111111111100101110'" (* 2096942 (0x1fff2e) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~1~0).
 Notation "'0b111111111111111001010'" (* 2097098 (0x1fffca) *)
@@ -1247,12 +1255,16 @@ Notation "'0b1111111110100111111110'" (* 4188670 (0x3fe9fe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~0~1~0~0~1~1~1~1~1~1~1~1~0).
 Notation "'0b1111111111011111111110'" (* 4192254 (0x3ff7fe) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~0).
+Notation "'0b1111111111101110001110'" (* 4193166 (0x3ffb8e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
 Notation "'0b1111111111110000101111'" (* 4193327 (0x3ffc2f) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~0~1~1~1~1).
 Notation "'0b1111111111110100000011'" (* 4193539 (0x3ffd03) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1).
 Notation "'0b1111111111110111000111'" (* 4193735 (0x3ffdc7) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1).
+Notation "'0b1111111111111000011111'" (* 4193823 (0x3ffe1f) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
 Notation "'0b1111111111111001011011'" (* 4193883 (0x3ffe5b) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1).
 Notation "'0b1111111111111011000011'" (* 4193987 (0x3ffec3) *)
@@ -1303,10 +1315,14 @@ Notation "'0b11111111111101000000110'" (* 8387078 (0x7ffa06) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~0~0~0~0~0~1~1~0).
 Notation "'0b11111111111101110001110'" (* 8387470 (0x7ffb8e) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~0~0~0~1~1~1~0).
+Notation "'0b11111111111110000111110'" (* 8387646 (0x7ffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0b11111111111110010110110'" (* 8387766 (0x7ffcb6) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1~0).
 Notation "'0b11111111111110110000110'" (* 8387974 (0x7ffd86) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~0~0~0~0~1~1~0).
+Notation "'0b11111111111111000011111'" (* 8388127 (0x7ffe1f) *)
+  := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1).
 Notation "'0b11111111111111001011011'" (* 8388187 (0x7ffe5b) *)
   := (Const WO~0~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1).
 Notation "'0b11111111111111010000110'" (* 8388230 (0x7ffe86) *)
@@ -1367,6 +1383,8 @@ Notation "'0b111111101111111111111111'" (* 16711679 (0xfeffff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1).
 Notation "'0b111111111111101011111111'" (* 16775935 (0xfffaff) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1).
+Notation "'0b111111111111110000111110'" (* 16776254 (0xfffc3e) *)
+  := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1~1~1~1~1~0).
 Notation "'0b111111111111110010110110'" (* 16776374 (0xfffcb6) *)
   := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~1~0~1~1~0~1~1~0).
 Notation "'0b111111111111110110000110'" (* 16776582 (0xfffd86) *)