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

---
 src/pretty_print_coq.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src')

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