aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ec81a3f1a..8ae6ac2bc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -929,10 +929,12 @@ let vernac_chdir = function
let vernac_write_state file =
Pfedit.delete_all_proofs ();
+ let file = CUnix.make_suffix file ".coq" in
States.extern_state file
let vernac_restore_state file =
Pfedit.delete_all_proofs ();
+ let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in
States.intern_state file
(************)