Option -v8 à coqtop lance coqtopnew; option -no-strict; option -no-proofs

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

5 files changed, 31 insertions, 16 deletions

diff --git a/lib/options.ml b/lib/options.ml
index 5725395724..135673a821 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -34,7 +34,7 @@ let translate = ref false
 let make_translate f = translate := f; v7 := f; ()
 let do_translate () = !translate
 let translate_file = ref false
-let p1 = ref true
+let translate_strict_impargs = ref true
 
 (* True only when interning from pp*new.ml *)
 let translate_syntax = ref false
diff --git a/lib/options.mli b/lib/options.mli
index db6ee1d5bd..41e8dea844 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -32,8 +32,8 @@ val translate : bool ref
 val make_translate : bool -> unit
 val do_translate : unit -> bool
 val translate_file : bool ref
-val p1 : bool ref
 val translate_syntax : bool ref
+val translate_strict_impargs : bool ref
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index 641a3cf6d7..324b291b57 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -129,7 +129,7 @@ let parse_args () =
     | ("-libdir"|"-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file"|"-dump-glob" as o) :: rem ->
+      |"-init-file"|"-dump-glob"|"-no-strict" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 7ea045136c..a7de40633d 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -81,7 +81,10 @@ let init_load_path () =
   if Sys.file_exists user_contrib then 
     Mltop.add_path user_contrib Nameops.default_root_prefix;
   (* then standard library *)
-  let dirs = "states" :: dev @ [ "theories"; "tactics"; "contrib"; "ide" ] in
+  let vdirs = 
+    if !Options.v7 then [ "theories"; "contrib" ]
+    else [ "newtheories"; "newcontrib" ] in
+  let dirs = "states" :: dev @ vdirs @ [ "ide" ] in
   List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d67dd0dfdc..199a520c88 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,9 +35,14 @@ let set_batch_mode () = batch_mode := true
 
 let remove_top_ml () = Mltop.remove ()
 
-let inputstate = ref "initial.coq"
-let set_inputstate s = inputstate:= s
-let inputstate () = if !inputstate <> "" then intern_state !inputstate
+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 (if !Options.v7 then "initial.coq" else "initialnew.coq")
 
 let outputstate = ref ""
 let set_outputstate s = outputstate:=s
@@ -87,11 +92,18 @@ let set_opt () = re_exec_version := "opt"
 let re_exec () =
   let s = !re_exec_version in
   let is_native = (Mltop.get()) = Mltop.Native in
-  if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin
-    let prog = Sys.argv.(0) in
+  let mustbe_v8 = not !Options.v7 in
+  let prog = Sys.argv.(0) in
+  let coq = Filename.basename prog in
+  let is_v8 = coq = "coqtopnew.byte" or coq = "coqtopnew.opt" in
+  if (is_native && s = "byte") || ((not is_native) && s = "opt")
+    || (is_v8 <> mustbe_v8)
+  then begin
+    let s = if s = "" then if is_native then "opt" else "byte" else s in
     let newprog = 
       let dir = Filename.dirname prog in
-      let com = "coqtop." ^ s ^ Coq_config.exec_extension in
+      let coqtop = if mustbe_v8 then "coqtopnew." else "coqtop." in
+      let com = coqtop ^ s ^ Coq_config.exec_extension in
       if dir <> "." then Filename.concat dir com else com 
     in
     Sys.argv.(0) <- newprog;
@@ -165,18 +177,14 @@ let parse_args is_ide =
     | "-compile-verbose" :: f :: rem -> add_compile true f; parse rem
     | "-compile-verbose" :: []       -> usage ()
 
+    | "-no-proofs" :: rem -> Options.dont_load_proofs := true; parse rem
+
     | "-translate" :: rem -> make_translate true; parse rem
     | "-ftranslate" :: rem ->
         make_translate true;
         translate_file := true;
         parse rem
 
-    | "-translate2" :: rem -> make_translate true; p1:=false; parse rem
-    | "-ftranslate2" :: rem ->
-        make_translate true; p1:= false;
-        translate_file := true;
-        parse rem
-
     | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
 
@@ -214,6 +222,10 @@ let parse_args is_ide =
        Impargs.make_strict_implicit_args true;
        parse rem
 
+    (* Translator options *)
+    | "-no-strict" :: rem -> 
+	Options.translate_strict_impargs := false; parse rem
+
     | s :: rem -> 
 	if is_ide then begin
 	  ide_args := s :: !ide_args;