diff options
| -rw-r--r-- | toplevel/coqtop.ml | 11 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
2 files changed, 12 insertions, 5 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2d6a9f2af..5ece34630 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -63,11 +63,16 @@ let require () = let re_exec s = let is_native = (Mltop.get()) = Mltop.Native in - if (is_native && s = "byte") || ((not is_native) && s = "opt") then + if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let prog = Sys.argv.(0) in - let newprog = Filename.concat (Filename.dirname prog) ("coqtop." ^ s) in + let newprog = + let dir = Filename.dirname prog in + let com = "coqtop." ^ s in + if dir <> "." then Filename.concat dir com else com + in Sys.argv.(0) <- newprog; - Unix.execv newprog Sys.argv + Unix.execvp newprog Sys.argv + end (* Parsing of the command line. * diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 54fcda305..47675e0df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -811,7 +811,8 @@ let _ = definition_body_red red_option id (local,stre) c typ_opt; if coe then begin Class.try_add_new_coercion id stre; - message ((string_of_id id) ^ " is now a coercion") + if (not (is_silent())) then + message ((string_of_id id) ^ " is now a coercion") end; if idcoe then Class.try_add_new_coercion_subclass id stre; @@ -1247,7 +1248,8 @@ let _ = let isid = identity = "IDENTITY" in fun () -> Class.try_add_new_coercion_with_target id stre ids idt isid; - message ((string_of_id id) ^ " is now a coercion") + if (not (is_silent())) then + message ((string_of_id id) ^ " is now a coercion") | _ -> bad_vernac_args "COERCION") let _ = |