From d2ddaad22f25a152d5fd53c11b3e1698747bd9c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 4 Jul 2018 11:43:06 +0100
Subject: Coq: turn off partial support for dropping true constraints, fix
 strings

---
 src/pretty_print_coq.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 78507577..6df8c5df 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -424,7 +424,7 @@ let doc_typ, doc_atomic_typ =
            List.fold_left add_tyvar tpp kids
         | None ->
            match nc with
-           | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)
+(*           | NC_aux (NC_true,_) -> List.fold_left add_tyvar (string "Z") (List.tl kids)*)
            | _ -> List.fold_left add_tyvar (doc_arithfact ctx nc) kids
       end
     and doc_typ_arg (Typ_arg_aux(t,_)) = match t with
@@ -1839,6 +1839,8 @@ try
           (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline;
         string "Import ListNotations.";
         hardline;
+        string "Open Scope string.";
+        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 *)
         string "Section Content.";
-- 
cgit v1.2.3