No more states/initial.coq, instead coqtop now requires Prelude.vo

 For starting a bare coqtop, the recommended option is now "-noinit"
 that skips the load of Prelude.vo. Option "-nois" is kept for
 compatibility, it is now an alias to "-noinit".

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

3 files changed, 11 insertions, 12 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 11c082e12..eac009984 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -96,7 +96,7 @@ let init_load_path () =
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs (fun x -> msg_warning (str x)) in
   let coqpath = Envars.coqpath in
-  let dirs = ["states";"plugins"] in
+  let dirs = ["plugins"] in
     (* NOTE: These directories are searched from last to first *)
     (* first, developer specific directory to open *)
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
@@ -104,7 +104,7 @@ let init_load_path () =
     List.iter
       (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
       theories_dirs_map;
-    (* then states and plugins *)
+    (* then plugins *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
     (* then user-contrib *)
     if Sys.file_exists user_contrib then
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f76558911..cd7da30bb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -63,13 +63,9 @@ let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
-let inputstate = ref None
-let set_inputstate s = inputstate:= Some s
-let inputstate () =
-  match !inputstate with
-    | Some "" -> ()
-    | Some s -> intern_state s
-    | None -> intern_state "initial.coq"
+let inputstate = ref ""
+let set_inputstate s = inputstate:=s
+let inputstate () = if !inputstate <> "" then intern_state !inputstate
 
 let outputstate = ref ""
 let set_outputstate s = outputstate:=s
@@ -101,11 +97,13 @@ let load_vernac_obj () =
   List.iter (fun f -> Library.require_library_from_file None f None)
     (List.rev !load_vernacular_obj)
 
+let load_init = ref true
+
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
   List.iter (fun s -> Library.require_library_from_file None s (Some false))
-    (List.rev !require_list)
+    ((if !load_init then ["Prelude"] else []) @ List.rev !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
 let add_compile verbose s =
@@ -196,7 +194,7 @@ let parse_args arglist =
       Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
-    | "-nois" :: rem -> set_inputstate ""; parse rem
+    | ("-noinit"|"-nois") :: rem -> load_init := false; parse rem
 
     | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
     | ("-inputstate"|"-is") :: []       -> usage ()
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2ddd42d7b..4751f7e32 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -27,9 +27,10 @@ let print_usage_channel co command =
 \n  -notop                 set the toplevel name to be the empty logical path\
 \n  -exclude-dir f         exclude subdirectories named f for option -R\
 \n\
+\n  -noinit                start without loading the Init library\
+\n  -nois                  (idem)\
 \n  -inputstate f          read state from file f.coq\
 \n  -is f                  (idem)\
-\n  -nois                  start with an empty state\
 \n  -outputstate f         write state in file f.coq\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
 \n  -verbose-compat-notations  be warned when using compatibility notations\