aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--toplevel/coqtop.ml12
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6cb8ddb29b..85a289ff36 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -61,7 +61,11 @@ let add_load_vernacular s =
load_vernacular_list := (make_suffix s ".v") :: !load_vernacular_list
let load_vernacular () =
List.iter
- (fun s -> with_option translate_file (Vernac.load_vernac false) s)
+ (fun s ->
+ if Options.do_translate () then
+ with_option translate_file (Vernac.load_vernac false) s
+ else
+ Vernac.load_vernac false s)
(List.rev !load_vernacular_list)
let load_vernacular_obj = ref ([] : string list)
@@ -82,7 +86,11 @@ let add_compile verbose s =
compile_list := (verbose,s) :: !compile_list
let compile_files () =
List.iter
- (fun (v,f) -> with_option translate_file (Vernac.compile v) f)
+ (fun (v,f) ->
+ if Options.do_translate () then
+ with_option translate_file (Vernac.compile v) f
+ else
+ Vernac.compile v f)
(List.rev !compile_list)
let re_exec_version = ref ""