diff options
| author | Brian Campbell | 2018-06-20 14:28:18 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-06-20 18:21:27 +0100 |
| commit | 45c062939ffcdb423774ed1af5266f9b779b2c6a (patch) | |
| tree | cf9a91925c40c7443e0ef893a8cad47d9fa68575 /lib | |
| parent | 835d3948e4209e38902e9f785301e3c3de93dd50 (diff) | |
Coq: Tidy up libraries, export String
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_values.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index c211cfdc..c3acbbcb 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1,11 +1,11 @@ (* Version of sail_values.lem that uses Lems machine words library *) (*Require Import Sail_impl_base*) -Require Import ZArith. Require Export ZArith. -Require Import String. +Require Export String. Require Import bbv.Word. -Require Import List. +Require Export List. +Require Export Sumbool. Import ListNotations. Open Scope Z. |
