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 | |
| parent | 835d3948e4209e38902e9f785301e3c3de93dd50 (diff) | |
Coq: Tidy up libraries, export String
| -rw-r--r-- | lib/coq/Sail2_values.v | 6 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
2 files changed, 4 insertions, 5 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. diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 8b479b6f..2e07dea7 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1742,7 +1742,6 @@ try [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline; -string "Require Import String."; hardline; separate empty (List.map (doc_def unimplemented) typdefs); hardline; hardline; separate empty (List.map (doc_def unimplemented) statedefs); hardline; @@ -1758,7 +1757,7 @@ string "Require Import String."; hardline; [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline; -string "Require Import List. Import ListNotations. Require Import Sumbool."; + string "Import ListNotations."; hardline; (* Put the body into a Section so that we can define some values with Let to put them into the local context, where tactics can see them *) |