From 8a06df3ad1b90a355d3e5adb694002f00e67823e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 2 Aug 2018 15:58:45 +0100
Subject: Fill in more Coq builtins for aarch64

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

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 5752e6c0..6fcbbb52 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -54,7 +54,10 @@ Instance Decidable_eq_from_dec {T:Type} (eqdec: forall x y : T, {x = y} + {x <>
   Decidable_witness := proj1_sig (bool_of_sumbool (eqdec x y))
 }.
 destruct (eqdec x y); simpl; split; congruence.
-Qed.
+Defined.
+
+Instance Decidable_eq_string : forall (x y : string), Decidable (x = y) :=
+  Decidable_eq_from_dec String.string_dec.
 
 
 (* Project away range constraints in comparisons *)
-- 
cgit v1.2.3