aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/HexNotationConstants.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
-rw-r--r--src/Compilers/Z/HexNotationConstants.v5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v
index 16db5d8c7..635e3470b 100644
--- a/src/Compilers/Z/HexNotationConstants.v
+++ b/src/Compilers/Z/HexNotationConstants.v
@@ -132,6 +132,7 @@ nums = tuple(sorted(set(systematic_nums + [
134217690,
134217694,
134217697,
+ 134217698,
134217699,
134217703,
134217710,
@@ -1726,6 +1727,10 @@ Notation "'0x7ffffe1'" (* 134217697 (0x7ffffe1) *)
:= (Const 134217697%Z).
Notation "'0x7ffffe1'" (* 134217697 (0x7ffffe1) *)
:= (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~0~1).
+Notation "'0x7ffffe2'" (* 134217698 (0x7ffffe2) *)
+ := (Const 134217698%Z).
+Notation "'0x7ffffe2'" (* 134217698 (0x7ffffe2) *)
+ := (Const WO~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~0~0~1~0).
Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *)
:= (Const 134217699%Z).
Notation "'0x7ffffe3'" (* 134217699 (0x7ffffe3) *)