From 54a08099f2360372a1e94f9ed0489a1dc89351af Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 13 Jun 2019 18:01:24 +0100
Subject: Coq: add eq_bit built-in

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index bd22371a..e152fb67 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -385,6 +385,7 @@ Qed.
 Inductive bitU := B0 | B1 | BU.
 
 Scheme Equality for bitU.
+Definition eq_bit := bitU_beq.
 Instance Decidable_eq_bit : forall (x y : bitU), Decidable (x = y) :=
   Decidable_eq_from_dec bitU_eq_dec.
 
-- 
cgit v1.2.3