From 45c062939ffcdb423774ed1af5266f9b779b2c6a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 20 Jun 2018 14:28:18 +0100
Subject: Coq: Tidy up libraries, export String

---
 lib/coq/Sail2_values.v  | 6 +++---
 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 *)
-- 
cgit v1.2.3