From c6a03fe03e9e19978cceb64562acfffd7ca066ea Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 13 Sep 2018 16:44:46 +0100
Subject: Coq: make generic_neq work on real

---
 lib/coq/Sail2_real.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/lib/coq/Sail2_real.v b/lib/coq/Sail2_real.v
index 49023d4c..23070935 100644
--- a/lib/coq/Sail2_real.v
+++ b/lib/coq/Sail2_real.v
@@ -1,6 +1,11 @@
 Require Export Rbase.
 Require Import Reals.
 Require Export ROrderedType.
+Require Import Sail2_values.
+
+(* "Decidable" in a classical sense... *)
+Instance Decidable_eq_real : forall (x y : R), Decidable (x = y) :=
+  Decidable_eq_from_dec Req_dec.
 
 Definition realFromFrac (num denom : Z) : R := Rdiv (IZR num) (IZR denom).
 
-- 
cgit v1.2.3