Coq: project away range types in comparisons

1 files changed, 9 insertions, 0 deletions

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 23e7f486..7c70f88b 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -22,6 +22,15 @@ Defined.
 Definition build_ex (n:Z) {P:Z -> Prop} `{H:ArithFact (P n)} : {x : Z & ArithFact (P x)} :=
   existT _ n H.
 
+(* Project away range constraints in comparisons *)
+Definition ltb_range_l {P} (l : sigT P) r := Z.ltb (projT1 l) r.
+Definition leb_range_l {P} (l : sigT P) r := Z.leb (projT1 l) r.
+Definition gtb_range_l {P} (l : sigT P) r := Z.gtb (projT1 l) r.
+Definition geb_range_l {P} (l : sigT P) r := Z.geb (projT1 l) r.
+Definition ltb_range_r {P} l (r : sigT P) := Z.ltb l (projT1 r).
+Definition leb_range_r {P} l (r : sigT P) := Z.leb l (projT1 r).
+Definition gtb_range_r {P} l (r : sigT P) := Z.gtb l (projT1 r).
+Definition geb_range_r {P} l (r : sigT P) := Z.geb l (projT1 r).
 
 Definition ii := Z.
 Definition nn := nat.