diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/options.ml | 12 | ||||
| -rw-r--r-- | lib/options.mli | 3 |
2 files changed, 1 insertions, 14 deletions
diff --git a/lib/options.ml b/lib/options.ml index 38c6e91a1..854e302f8 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -31,19 +31,9 @@ let dont_load_proofs = ref false let raw_print = ref false -let v7 = - let transl = array_exists ((=) "-translate") Sys.argv in - let v7 = array_exists ((=) "-v7") Sys.argv in - let v8 = array_exists ((=) "-v8") Sys.argv in - if v8 & transl then error "Options -translate and -v8 are incompatible"; - if v8 & v7 then error "Options -v7 and -v8 are incompatible"; - ref (v7 or transl) - -let v7_only = ref false - (* Translate *) let translate = ref false -let make_translate f = translate := f; v7 := f; () +let make_translate f = translate := f let do_translate () = !translate let translate_file = ref false let translate_strict_impargs = ref true diff --git a/lib/options.mli b/lib/options.mli index d415f93d0..9eea81ed3 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -26,9 +26,6 @@ val dont_load_proofs : bool ref val raw_print : bool ref -val v7 : bool ref -val v7_only : bool ref - val translate : bool ref val make_translate : bool -> unit val do_translate : unit -> bool |