compat ocaml 3.03

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

7 files changed, 73 insertions, 66 deletions

diff --git a/library/declare.ml b/library/declare.ml
index c87ec0d34..2b86f8954 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -84,17 +84,17 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.init_function = (fun () -> vartab := Idmap.empty);
 	    Summary.survive_section = false }
 
-let cache_variable (sp,(id,(p,d,str))) =
+let cache_variable (sp,(id,(p,d,strength))) =
   (* Constr raisonne sur les noms courts *)
   if Idmap.mem id !vartab then
-    errorlabstrm "cache_variable" [< pr_id id; 'sTR " already exists" >];
+    errorlabstrm "cache_variable" (pr_id id ++ str " already exists");
   let cst = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ty -> Global.push_named_assum (id,ty)
     | SectionLocalDef (c,t) -> Global.push_named_def (id,c,t) in
   let (_,bd,ty) = Global.lookup_named id in
   let vd = (bd,ty,cst) in
   Nametab.push 0 (restrict_path 0 sp) (VarRef id);
-  vartab := Idmap.add id (p,vd,str) !vartab
+  vartab := Idmap.add id (p,vd,strength) !vartab
 
 let (in_variable, out_variable) =
   let od = {
@@ -125,7 +125,7 @@ let _ = Summary.declare_summary "CONSTANT"
 let cache_constant (sp,(cdt,stre)) =
   (if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   Global.add_constant sp cdt;
   (match stre with
     | DischargeAt (dp,n) when not (is_dirpath_prefix_of dp (Lib.cwd ())) ->
@@ -143,7 +143,7 @@ let cache_constant (sp,(cdt,stre)) =
 let load_constant (sp,(ce,stre)) =
   (if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "cache_constant" [< pr_id id; 'sTR " already exists" >]);
+    errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   csttab := Spmap.add sp stre !csttab;
   Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp)
 
@@ -206,7 +206,7 @@ let inductive_names sp mie =
 let check_exists_inductive (sp,_) =
   if Nametab.exists_cci sp then
     let (_,id) = repr_path sp in
-    errorlabstrm "cache_inductive" [< pr_id id; 'sTR " already exists" >]
+    errorlabstrm "cache_inductive" (pr_id id ++ str " already exists")
 
 let cache_inductive (sp,mie) =
   let names = inductive_names sp mie in
diff --git a/library/goptions.ml b/library/goptions.ml
index 95336c35e..f919b12e8 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -109,10 +109,11 @@ module MakeTable =
          (fun c -> t := MySet.remove c !t))
 
     let print_table table_name printer table =
-      mSG ([< 'sTR table_name ; (hOV 0 
-           (if MySet.is_empty table then [< 'sTR "None" ; 'fNL >]
-            else MySet.fold
-	      (fun a b -> [< printer a; 'sPC; b >]) table [<>])) >])
+      msg (str table_name ++ 
+	   (hov 0 
+	      (if MySet.is_empty table then str "None" ++ fnl ()
+               else MySet.fold
+		 (fun a b -> printer a ++ spc () ++ b) table (mt ()))))
 
     class table_of_A () =
     object
@@ -123,7 +124,7 @@ module MakeTable =
       method remove x = remove_option (A.encode x)
       method mem x = 
         let answer = MySet.mem (A.encode x) !t in
-        mSG [< 'sTR (A.member_message x answer) >]
+        msg (str (A.member_message x answer))
       method print = print_table A.title A.printer !t 
     end
 
@@ -152,7 +153,7 @@ struct
   let table = string_table
   let encode x = x
   let check = A.check
-  let printer s = [< 'sTR s >]
+  let printer s = (str s)
   let key = A.key
   let title = A.title
   let member_message = A.member_message
@@ -298,10 +299,10 @@ let set_string_option_value = set_option_value
 
 let msg_option_value (name,v) =
   match v with
-    | BoolValue true  -> [< 'sTR "true" >]
-    | BoolValue false -> [< 'sTR "false" >]
-    | IntValue n      -> [< 'iNT n >]
-    | StringValue s   -> [< 'sTR s >]
+    | BoolValue true  -> str "true"
+    | BoolValue false -> str "false"
+    | IntValue n      -> int n
+    | StringValue s   -> str s
     | IdentValue r    -> pr_global_env (Global.env()) r
 
 let print_option_value key =
@@ -309,35 +310,41 @@ let print_option_value key =
   let s = read () in 
   match s with
     | BoolValue b -> 
-	mSG [< 'sTR("The "^name^" mode is "^(if b then "on" else "off"));'fNL>]
+	msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ 
+	     fnl ())
     | _ ->
-	mSG [< 'sTR ("Current value of "^name^" is "); 
-	       msg_option_value (name,s); 'fNL >]
+	msg (str ("Current value of "^name^" is ") ++
+	     msg_option_value (name,s) ++ fnl ())
 
 
 let print_tables () =
-  mSG
-  [< 'sTR "Synchronous options:"; 'fNL; 
+  msg
+    (str "Synchronous options:" ++ fnl () ++
      OptionMap.fold 
        (fun key (name,(sync,read,write)) p -> 
-	  if sync then [< p; 'sTR ("  "^(nickname key)^": ");
-			  msg_option_value (name,read()); 'fNL >]
-	  else [< p >])
-       !value_tab [<>];
-     'sTR "Asynchronous options:"; 'fNL;
+	  if sync then 
+	    p ++ str ("  "^(nickname key)^": ") ++
+	    msg_option_value (name,read()) ++ fnl ()
+	  else 
+	    p)
+       !value_tab (mt ()) ++
+     str "Asynchronous options:" ++ fnl () ++
      OptionMap.fold 
        (fun key (name,(sync,read,write)) p -> 
-	  if sync then [< p >] 
-	  else [< p; 'sTR ("  "^(nickname key)^": ");
-                  msg_option_value (name,read()); 'fNL >])
-       !value_tab [<>];
-     'sTR "Tables:"; 'fNL;
+	  if sync then 
+	    p
+	  else 
+	    p ++ str ("  "^(nickname key)^": ") ++
+            msg_option_value (name,read()) ++ fnl ())
+       !value_tab (mt ()) ++
+     str "Tables:" ++ fnl () ++
      List.fold_right
-       (fun (nickkey,_) p -> [< p; 'sTR ("  "^nickkey); 'fNL >])
-       !string_table [<>];
+       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+       !string_table (mt ()) ++
      List.fold_right
-       (fun (nickkey,_) p -> [< p; 'sTR ("  "^nickkey); 'fNL >])
-       !ident_table [<>];
-     'fNL;
- >]
+       (fun (nickkey,_) p -> p ++ str ("  "^nickkey) ++ fnl ())
+       !ident_table (mt ()) ++
+     fnl ()
+    )
+
 
diff --git a/library/lib.ml b/library/lib.ml
index f989ce988..8eaba772e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -147,7 +147,7 @@ let open_section id =
   let dir = extend_dirpath !path_prefix id in
   let sp = make_path id in
   if Nametab.exists_section dir then
-    errorlabstrm "open_section" [< pr_id id; 'sTR " already exists" >];
+    errorlabstrm "open_section" (pr_id id ++ str " already exists");
   let sum = freeze_summaries() in
   add_entry sp (OpenedSection (dir, sum));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
@@ -176,7 +176,7 @@ let export_segment seg =
 
 (* Restore lib_stk and summaries as before the section opening, and
    add a ClosedSection object. *)
-let close_section export id =
+let close_section ~export id =
   let sp,dir,fs = 
     try match find_entry_p is_opened_section with
       | sp,OpenedSection (dir,fs) -> 
diff --git a/library/library.ml b/library/library.ml
index 970c2f6bf..5dc120c23 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -246,9 +246,9 @@ let with_magic_number_check f a =
   try f a
   with System.Bad_magic_number fname ->
     errorlabstrm "load_module_from"
-    [< 'sTR"file "; 'sTR fname; 'sPC; 'sTR"has bad magic number.";
-    'sPC; 'sTR"It is corrupted"; 'sPC;
-    'sTR"or was compiled with another version of Coq." >]
+    (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
+    spc () ++ str"It is corrupted" ++ spc () ++
+    str"or was compiled with another version of Coq.")
 
 let rec load_module = function
   | (LibLoaded, dir, _) ->
@@ -264,9 +264,9 @@ let rec load_module = function
       close_in ch;
       if dir <> md.md_name then
 	errorlabstrm "load_module"
-	  [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
-	  pr_dirpath md.md_name; 'sPC; 'sTR "and not module"; 'sPC;
-	  pr_dirpath dir >];
+	  (str ("The file " ^ f ^ " contains module") ++ spc () ++
+	  pr_dirpath md.md_name ++ spc () ++ str "and not module" ++ spc () ++
+	  pr_dirpath dir);
       compunit_cache := Stringmap.add f (md, digest) !compunit_cache;
       (md, digest) in
     intern_module digest f md
@@ -301,11 +301,11 @@ and load_absolute_module_from dir =
   | LibUnmappedDir ->
       let prefix, dir = fst (split_dirpath dir), string_of_dirpath dir in
       errorlabstrm "load_module"
-      [< 'sTR ("Cannot load "^dir^":"); 'sPC; 
-      'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+      (str ("Cannot load "^dir^":") ++ spc () ++ 
+      str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
   | LibNotFound ->
       errorlabstrm "load_module"
-      [< 'sTR"Cannot find module "; pr_dirpath dir; 'sTR" in loadpath">]
+      (str"Cannot find module " ++ pr_dirpath dir ++ str" in loadpath")
   | e -> raise e
 
 let locate_qualified_library qid =
@@ -336,19 +336,19 @@ let try_locate_qualified_library qid =
   | LibUnmappedDir ->
       let prefix, id = repr_qualid qid in
       errorlabstrm "load_module"
-      [< 'sTR ("Cannot load "^(string_of_id id)^":"); 'sPC; 
-      'sTR "no physical path bound to"; 'sPC; pr_dirpath prefix; 'fNL >]
+      (str ("Cannot load "^(string_of_id id)^":") ++ spc () ++ 
+      str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
   | LibNotFound ->
       errorlabstrm "load_module"
-      [< 'sTR"Cannot find module "; pr_qualid qid; 'sTR" in loadpath">]
+      (str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath")
   | _ -> assert false
 
 let check_module_short_name f dir = function
   | Some id when id <> snd (split_dirpath dir) ->
       errorlabstrm "load_module"
-      [< 'sTR ("The file " ^ f ^ " contains module"); 'sPC;
-      pr_dirpath dir; 'sPC; 'sTR "and not module"; 'sPC;
-      pr_id id >]
+      (str ("The file " ^ f ^ " contains module") ++ spc () ++
+      pr_dirpath dir ++ spc () ++ str "and not module" ++ spc () ++
+      pr_id id)
   | _ -> ()
 
 let locate_by_filename_only id f =
@@ -473,10 +473,10 @@ let iter_all_segments insec f =
 let fmt_modules_state () =
   let opened = opened_modules ()
   and loaded = loaded_modules () in
-  [< 'sTR "Imported (open) Modules: " ;
-     prlist_with_sep pr_spc pr_dirpath opened ; 'fNL ;
-     'sTR "Loaded Modules: ";
-     prlist_with_sep pr_spc pr_dirpath loaded ; 'fNL >]
+  (str "Imported (open) Modules: " ++
+     prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++
+     str "Loaded Modules: " ++
+     prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ())
 
 (*s Display the memory use of a module. *)
 
@@ -484,6 +484,6 @@ open Printf
 
 let mem s =
   let m = find_module s in
-  h 0 [< 'sTR (sprintf "%dk (cenv = %dk / seg = %dk)"
+  h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
 		 (size_kb m) (size_kb m.module_compiled_env) 
-		 (size_kb m.module_declarations)) >]
+		 (size_kb m.module_declarations)))
diff --git a/library/nameops.ml b/library/nameops.ml
index c748f5a55..ecbe07e77 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -17,7 +17,7 @@ open Term
 
 (* Identifiers *)
 
-let pr_id id = [< 'sTR (string_of_id id) >]
+let pr_id id = (str (string_of_id id))
 
 let wildcard = id_of_string "_"
 
@@ -145,7 +145,7 @@ let next_name_away name l =
 
 (**********************************************)
 
-let pr_dirpath sl = [< 'sTR (string_of_dirpath sl) >]
+let pr_dirpath sl = (str (string_of_dirpath sl))
 
 (* Operations on dirpaths *)
 let empty_dirpath = make_dirpath []
@@ -234,4 +234,4 @@ let path_of_string s =
     | Invalid_argument _ -> invalid_arg "path_of_string"
 
 (* Section paths *)
-let pr_sp sp = [< 'sTR (string_of_path sp) >]
+let pr_sp sp = (str (string_of_path sp))
diff --git a/library/nametab.ml b/library/nametab.ml
index f70d672f8..99524bde1 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -157,7 +157,7 @@ let push_long_names_libpath = push_modidtree the_libtab
    possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
    Parameter but also Remark and Fact) *)
 
-let push_cci n sp ref =
+let push_cci ~visibility:n sp ref =
   let dir, s = repr_path sp in
   (* We push partially qualified name (with at least one prefix) *)
   push_long_names_ccipath n dir s (TrueGlobal ref)
@@ -297,7 +297,7 @@ let pr_global_env env ref =
   paresseusement : il faut forcer l'évaluation pour capturer
   l'éventuelle levée d'une exception (le cas échoit dans le debugger) *)
   let s = string_of_qualid (shortest_qualid_of_global env ref) in
-  [< 'sTR s >]
+  (str s)
 
 (********************************************************************)
 
diff --git a/library/summary.ml b/library/summary.ml
index c315e0cd2..210a1a81b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -34,7 +34,7 @@ let declare_summary sumname sdecl =
   in
   if Hashtbl.mem summaries sumname then
     anomalylabstrm "Summary.declare_summary"
-      [< 'sTR "Cannot declare a summary twice: " ; 'sTR sumname >];
+      (str "Cannot declare a summary twice: " ++ str sumname);
   Hashtbl.add summaries sumname ddecl
 
 type frozen = Dyn.t Stringmap.t