diff options
| author | herbelin | 2005-12-26 13:51:24 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-26 13:51:24 +0000 |
| commit | e0f9487be5ce770117a9c9c815af8c7010ff357b (patch) | |
| tree | bbbde42b0a40803a0c5f5bdb5aaf09248d9aedc0 /lib | |
| parent | 98d60ce261e7252379ced07d2934647c77efebfd (diff) | |
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
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 38c6e91a18..854e302f8c 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 d415f93d0e..9eea81ed30 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 |