diff options
Diffstat (limited to 'lib/options.ml')
| -rw-r--r-- | lib/options.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml index b67f8359de..5725395724 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -24,6 +24,8 @@ let term_quality = ref false let xml_export = ref false +let dont_load_proofs = ref false + let v7 = ref true let v7_only = ref false @@ -34,6 +36,9 @@ let do_translate () = !translate let translate_file = ref false let p1 = ref true +(* True only when interning from pp*new.ml *) +let translate_syntax = ref false + (* Silent / Verbose *) let silent = ref false let make_silent flag = silent := flag; () |