From 78d1c75322684eaa7e0ef753ee56d9c6140ec830 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 13 Dec 2001 09:03:13 +0000 Subject: compat ocaml 3.03 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declare.ml | 12 +++++----- library/goptions.ml | 69 +++++++++++++++++++++++++++++------------------------ library/lib.ml | 4 ++-- library/library.ml | 42 ++++++++++++++++---------------- library/nameops.ml | 6 ++--- library/nametab.ml | 4 ++-- library/summary.ml | 2 +- 7 files changed, 73 insertions(+), 66 deletions(-) (limited to 'library') 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 -- cgit v1.2.3