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 /src | |
| parent | 835d3948e4209e38902e9f785301e3c3de93dd50 (diff) | |
Coq: Tidy up libraries, export String
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
1 files changed, 1 insertions, 2 deletions
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 *) |