diff options
| author | Brian Campbell | 2020-01-21 11:54:34 +0000 |
|---|---|---|
| committer | Brian Campbell | 2020-01-21 14:10:26 +0000 |
| commit | 9f9d4e5e9662e7a173fa870632299a752fd204c4 (patch) | |
| tree | 3966d4ceae6fff658a7262059351386cbf3730ce /lib | |
| parent | 8e8df51b58b1ae0451ddb6b1d624d37ed064ba45 (diff) | |
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.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |