From 9f9d4e5e9662e7a173fa870632299a752fd204c4 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 21 Jan 2020 11:54:34 +0000
Subject: Use hex/bin literals in Coq backend Also be more careful to avoid
 pattern bindings with identifiers to avoid parsing clashes, eg `let 'bytes :=
 ...` which is confused with the notation for binary literals.

---
 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 48920a59..9b76ce62 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -5,6 +5,7 @@ Require Export ZArith.
 Require Import Ascii.
 Require Export String.
 Require Import bbv.Word.
+Require Export bbv.HexNotationWord.
 Require Export List.
 Require Export Sumbool.
 Require Export DecidableClass.
-- 
cgit v1.2.3