aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/coqc.ml2
-rw-r--r--toplevel/coqtop.ml2
2 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml
index c6bb38e005..03c53d6991 100644
--- a/toplevel/coqc.ml
+++ b/toplevel/coqc.ml
@@ -11,7 +11,7 @@
let outputstate opts =
Option.iter (fun ostate_file ->
let fname = CUnix.make_suffix ostate_file ".coq" in
- Library.extern_state fname) opts.Coqcargs.outputstate
+ Vernacstate.System.dump fname) opts.Coqcargs.outputstate
let coqc_init _copts ~opts =
Flags.quiet := true;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 80123757ec..bbcfcc4826 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -52,7 +52,7 @@ let print_memory_stat () =
let inputstate opts =
Option.iter (fun istate_file ->
let fname = Loadpath.locate_file (CUnix.make_suffix istate_file ".coq") in
- Library.intern_state fname) opts.inputstate
+ Vernacstate.System.load fname) opts.inputstate
(******************************************************************************)
(* Fatal Errors *)