diff options
| author | herbelin | 2003-08-14 20:43:22 +0000 |
|---|---|---|
| committer | herbelin | 2003-08-14 20:43:22 +0000 |
| commit | 7374c787f4a2bb0d50e2d9348e559b1c94dfff5b (patch) | |
| tree | 6d26b9e249bbb6d8c19a2879cc405a1553ccacb0 /toplevel | |
| parent | 4135e812a99fdfd7404fd354f31f286a4b4f005a (diff) | |
Fusion -translate et -ftranslate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4276 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 199a520c88..5385644879 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -78,7 +78,9 @@ let add_compile verbose s = Options.make_silent true; compile_list := (verbose,s) :: !compile_list let compile_files () = - List.iter (fun (v,f) -> Vernac.compile v f) (List.rev !compile_list) + List.iter + (fun (v,f) -> with_option translate_file (Vernac.compile v) f) + (List.rev !compile_list) let re_exec_version = ref "" let set_byte () = re_exec_version := "byte" @@ -180,10 +182,6 @@ let parse_args is_ide = | "-no-proofs" :: rem -> Options.dont_load_proofs := true; parse rem | "-translate" :: rem -> make_translate true; parse rem - | "-ftranslate" :: rem -> - make_translate true; - translate_file := true; - parse rem | "-unsafe" :: f :: rem -> add_unsafe f; parse rem | "-unsafe" :: [] -> usage () |