Coq: turn off partial support for dropping true constraints, fix strings

1 files changed, 3 insertions, 1 deletions

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.";