Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 38 insertions, 28 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f5d1d142..a88ee3ba 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 11830 2009-01-22 06:45:13Z notin $ *)
+(* $Id$ *)
 
 open Pp
 open Util
@@ -21,7 +21,7 @@ open Coqinit
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib () in 
+    let coqlib = Envars.coqlib () in
     let ch = open_in (Filename.concat coqlib "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
@@ -37,7 +37,7 @@ let output_context = ref false
 
 let memory_stat = ref false
 
-let print_memory_stat () = 
+let print_memory_stat () =
   if !memory_stat then
     Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
 
@@ -47,7 +47,7 @@ let engagement = ref None
 let set_engagement c = engagement := Some c
 let engage () =
   match !engagement with Some c -> Global.set_engagement c | None -> ()
-  
+
 let set_batch_mode () = batch_mode := true
 
 let toplevel_default_name = make_dirpath [id_of_string "Top"]
@@ -72,22 +72,19 @@ let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
 let set_include d p =
   let p = dirpath_of_string p in
-  Library.check_coq_overwriting p;
   push_include (d,p)
 let set_rec_include d p =
-  let p = dirpath_of_string p in 
-  Library.check_coq_overwriting p;
+  let p = dirpath_of_string p in
   push_rec_include(d,p)
- 
+
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
   load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
 let load_vernacular () =
   List.iter
-    (fun (s,b) -> 
+    (fun (s,b) ->
       if Flags.do_beautify () then
 	with_option beautify_file (Vernac.load_vernac b) s
       else
@@ -96,7 +93,7 @@ let load_vernacular () =
 
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
-let load_vernac_obj () = 
+let load_vernac_obj () =
   List.iter (fun f -> Library.require_library_from_file None f None)
     (List.rev !load_vernacular_obj)
 
@@ -109,7 +106,7 @@ let require () =
 let compile_list = ref ([] : (bool * string) list)
 let add_compile verbose s =
   set_batch_mode ();
-  Flags.make_silent true; 
+  Flags.make_silent true;
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
@@ -124,6 +121,12 @@ let compile_files () =
 	   Vernac.compile v f)
       (List.rev !compile_list)
 
+let set_compat_version = function
+  | "8.2" -> compat_version := Some V8_2
+  | "8.1" -> warning "Compatibility with version 8.1 not supported."
+  | "8.0" -> warning "Compatibility with version 8.0 not supported."
+  | s -> error ("Unknown compatibility version \""^s^"\".")
+
 let re_exec_version = ref ""
 let set_byte () = re_exec_version := "byte"
 let set_opt () = re_exec_version := "opt"
@@ -145,11 +148,11 @@ let re_exec is_ide =
   if (is_native && s = "byte") || ((not is_native) && s = "opt")
   then begin
     let s = if s = "" then if is_native then "opt" else "byte" else s in
-    let newprog = 
+    let newprog =
       let dir = Filename.dirname prog in
       let coqtop = if is_ide then "coqide." else "coqtop." in
       let com = coqtop ^ s ^ Coq_config.exec_extension in
-      if dir <> "." then Filename.concat dir com else com 
+      if dir <> "." then Filename.concat dir com else com
     in
     Sys.argv.(0) <- newprog;
     Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
@@ -186,12 +189,12 @@ let parse_args is_ide =
   let glob_opt = ref false in
   let rec parse = function
     | [] -> ()
-    | "-with-geoproof" :: s :: rem -> 
+    | "-with-geoproof" :: s :: rem ->
 	if s = "yes" then Coq_config.with_geoproof := true
 	else if s = "no" then Coq_config.with_geoproof := false
 	else usage ();
 	parse rem
-    | "-impredicative-set" :: rem -> 
+    | "-impredicative-set" :: rem ->
         set_engagement Declarations.ImpredicativeSet; parse rem
 
     | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
@@ -218,13 +221,13 @@ let parse_args is_ide =
     | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
 
     | "-batch" :: rem -> set_batch_mode (); parse rem
-    | "-boot" :: rem -> boot := true; no_load_rc (); parse rem	     
+    | "-boot" :: rem -> boot := true; no_load_rc (); parse rem
     | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
     | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
     | "-nois" :: rem -> set_inputstate ""; parse rem
-	     
+
     | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
     | ("-inputstate"|"-is") :: []       -> usage ()
 
@@ -234,11 +237,11 @@ let parse_args is_ide =
     | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
     | "-load-ml-source" :: []       -> usage ()
 
-    | ("-load-vernac-source"|"-l") :: f :: rem -> 
+    | ("-load-vernac-source"|"-l") :: f :: rem ->
 	add_load_vernacular false f; parse rem
     | ("-load-vernac-source"|"-l") :: []       -> usage ()
 
-    | ("-load-vernac-source-verbose"|"-lv") :: f :: rem -> 
+    | ("-load-vernac-source-verbose"|"-lv") :: f :: rem ->
 	add_load_vernacular true f; parse rem
     | ("-load-vernac-source-verbose"|"-lv") :: []       -> usage ()
 
@@ -270,11 +273,14 @@ let parse_args is_ide =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
+    | "-compat" :: v :: rem -> set_compat_version v; parse rem
+    | "-compat" :: []       -> usage ()
+
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Flags.print_emacs := true; Pp.make_pp_emacs(); parse rem
-    | "-emacs-U" :: rem -> Flags.print_emacs := true; 
+    | "-emacs-U" :: rem -> Flags.print_emacs := true;
 	Flags.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
-	    
+
     | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
 
     | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
@@ -296,7 +302,9 @@ let parse_args is_ide =
     | "-user" :: u :: rem -> set_rcuser u; parse rem
     | "-user" :: []       -> usage ()
 
-    | "-notactics" :: rem -> remove_top_ml (); parse rem
+    | "-notactics" :: rem ->
+	warning "Obsolete option \"-notactics\".";
+	remove_top_ml (); parse rem
 
     | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
 
@@ -312,7 +320,7 @@ let parse_args is_ide =
 
     | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
 
-    | s :: rem -> 
+    | s :: rem ->
 	if is_ide then begin
 	  ide_args := s :: !ide_args;
 	  parse rem
@@ -322,7 +330,7 @@ let parse_args is_ide =
   in
   try
     parse (List.tl (Array.to_list Sys.argv))
-  with 
+  with
     | UserError(_,s) as e -> begin
 	try
 	  Stream.empty s; exit 1
@@ -359,17 +367,19 @@ let init is_ide =
       exit 1
   end;
   if !batch_mode then
-    (flush_all(); 
+    (flush_all();
      if !output_context then
        Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
-     Profile.print_profile (); 
+     Profile.print_profile ();
      exit 0);
   Lib.declare_initial_state ()
 
+let init_toplevel () = init false
+
 let init_ide () = init true; List.rev !ide_args
 
 let start () =
-  init false;
+  init_toplevel ();
   Toplevel.loop();
   (* Initialise and launch the Ocaml toplevel *)
   Coqinit.init_ocaml_path();