diff options
| -rw-r--r-- | toplevel/vernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7997b24516..735724aed0 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -132,7 +132,7 @@ and raw_compile_module verbosely only_spec mname file = if only_spec then failwith ".vi not yet implemented" else - Library.save_module_to mname base + Discharge.save_module_to mname base and read_vernac_file verbosely s = let interpfun = |