aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqc.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqc.ml')
-rw-r--r--toplevel/coqc.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index a403640149..b7af66b2ee 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -44,7 +44,7 @@ coqc specific options:\
let coqc_main ((copts,_),stm_opts) injections ~opts =
Topfmt.(in_phase ~phase:CompilationPhase)
- Ccompile.compile_files (opts,stm_opts) copts injections;
+ Ccompile.compile_file opts stm_opts copts injections;
(* Careful this will modify the load-path and state so after this
point some stuff may not be safe anymore. *)