diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
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."; |