- erreurs Pretype

 - Write / Restore State


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@230 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 27 insertions, 19 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 474b247a6..33ee012cf 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -56,19 +56,19 @@ let getenv_else s dft = try Sys.getenv s with Not_found -> dft
 
 (* Initializes the LoadPath according to COQLIB and Coq_config *)
 let init_load_path () =
-  (* default load path; only if COQLIB is defined *)
-  let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
-  let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
-  if coqlib = coqtop then
-    (* local installation *)
+  if Coq_config.local then
+    (* local use (no installation) *)
     List.iter 
-      (fun s -> add_include (Filename.concat coqtop s))
+      (fun s -> add_include (Filename.concat Coq_config.coqtop s))
       ("states" :: "dev" ::
        (List.map 
 	  (fun s -> Filename.concat "theories" (hm2 s))
           Coq_config.theories_dirs))
-  else
-    add_include coqlib;
+  else begin
+    (* default load path; only if COQLIB is defined *)
+    let coqlib = getenv_else "COQLIB" Coq_config.coqlib in
+    add_include coqlib
+  end;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_include camlp4;
   add_include ".";
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ce3b0e957..93a330316 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -219,25 +219,38 @@ let _ =
 (* Managing states *)
 
 let _ =
-  add "SaveState"
+  add "WriteState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> States.extern_state file)
+	   (fun () -> Pfedit.abort_refine States.extern_state file)
+       | [VARG_IDENTIFIER id] ->
+	   let file = string_of_id id in
+	   (fun () -> Pfedit.abort_refine States.extern_state file)
        | _ -> bad_vernac_args "SaveState")
 
 let _ =
-  add "LoadState"
+  add "RestoreState"
     (function 
        | [VARG_STRING file] ->
-	   (fun () -> States.intern_state file)
-       | _ -> bad_vernac_args "RestoreState")
+	   (fun () -> Pfedit.abort_refine States.intern_state file)
+       | [VARG_IDENTIFIER id] ->
+	   let file = string_of_id id in
+	   (fun () -> Pfedit.abort_refine States.intern_state file)
+       | _ -> bad_vernac_args "LoadState")
 
 (* Resetting *)
 
 let _ =
+  add "ResetName"
+    (function 
+       | [VARG_IDENTIFIER id] -> 
+	   (fun () -> Pfedit.abort_refine Lib.reset_name id)
+       | _ -> bad_vernac_args "ResetName")
+
+let _ =
   add "ResetInitial"
     (function 
-       | [] -> (fun () -> reset_initial ())
+       | [] -> (fun () -> Pfedit.abort_refine Lib.reset_initial ())
        | _  -> bad_vernac_args "ResetInitial")
 
 (***
@@ -249,11 +262,6 @@ let _ =
        | _ -> bad_vernac_args "ResetSection")
 
 ***)
-let _ =
-  add "ResetName"
-    (function 
-       | [VARG_IDENTIFIER id] -> (fun () -> Pfedit.reset_name id)
-       | _ -> bad_vernac_args "ResetName")
 
 (* Modules *)