aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.ml')
-rw-r--r--toplevel/coqinit.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 96a0bd5ec..3e7a83085 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -23,12 +23,12 @@ let set_debug () =
let rcdefaultname = "coqrc"
-let load_rcfile ~rcfile ~time ~state =
+let load_rcfile ~rcfile ~state =
try
match rcfile with
| Some rcfile ->
if CUnix.file_readable_p rcfile then
- Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state rcfile
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state rcfile
else raise (Sys_error ("Cannot read rcfile: "^ rcfile))
| None ->
try
@@ -39,7 +39,7 @@ let load_rcfile ~rcfile ~time ~state =
Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
Envars.home ~warn / "."^rcdefaultname
] in
- Vernac.load_vernac ~time ~echo:false ~interactive:false ~check:true ~state inferedrc
+ Vernac.load_vernac ~echo:false ~interactive:false ~check:true ~state inferedrc
with Not_found -> state
(*
Flags.if_verbose