From 2a2f38f46735a81a921891bf0bf9e35a7cc4a347 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Sat, 7 Jul 2018 15:17:20 +0100
Subject: Coq: eq_range should take proofs

---
 lib/coq/Sail2_values.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/coq')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 990817e6..db0339d8 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1368,6 +1368,8 @@ Definition abs_with_eq n   : {o : Z & ArithFact (o = Z.abs n)} := build_ex (Z.ab
 
 (* Similarly, for ranges (currently in MIPS) *)
 
+Definition eq_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)}) : bool :=
+  (projT1 l) =? (projT1 r).
 Definition add_range {n m o p} (l : {l & ArithFact (n <= l <= m)}) (r : {r & ArithFact (o <= r <= p)})
   : {x & ArithFact (n+o <= x <= m+p)} :=
   build_ex ((projT1 l) + (projT1 r)).
-- 
cgit v1.2.3