diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 17dba718..d0d13907 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -3311,6 +3311,10 @@ try (fun lib -> separate space [string "Require Import";string lib] ^^ dot) types_modules;hardline; string "Import ListNotations."; hardline; + string "Open Scope string."; hardline; + string "Open Scope bool."; hardline; + string "Open Scope Z."; hardline; + hardline; separate empty (List.map doc_def typdefs); hardline; hardline; separate empty (List.map doc_def statedefs); hardline; |