Delete trailing whitespaces in all *.{v,ml*} files

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

1 files changed, 40 insertions, 40 deletions

diff --git a/library/library.ml b/library/library.ml
index 831687723..9604a990c 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -39,7 +39,7 @@ let is_in_load_paths phys_dir =
   let dir = System.canonical_path_name phys_dir in
   let lp = get_load_paths () in
   let check_p = fun p -> (String.compare dir p) == 0 in
-    List.exists check_p lp 
+    List.exists check_p lp
 
 let remove_load_path dir =
   load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
@@ -48,7 +48,7 @@ let add_load_path isroot (phys_path,coq_path) =
   let phys_path = System.canonical_path_name phys_path in
     match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
       | [_,dir,_] ->
-	  if coq_path <> dir 
+	  if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
             (phys_path = System.canonical_path_name Filename.current_dir_name
@@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) =
 let physical_paths (dp,lp) = dp
 
 let extend_path_with_dirpath p dir =
-  List.fold_left Filename.concat p 
+  List.fold_left Filename.concat p
     (List.map string_of_id (List.rev (repr_dirpath dir)))
 
 let root_paths_matching_dir_path dir =
@@ -112,12 +112,12 @@ let loadpaths_matching_dir_path dir =
 let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
 
 (************************************************************************)
-(*s Modules on disk contain the following informations (after the magic 
+(*s Modules on disk contain the following informations (after the magic
     number, and before the digest). *)
 
 type compilation_unit_name = dir_path
 
-type library_disk = { 
+type library_disk = {
   md_name : compilation_unit_name;
   md_compiled : compiled_library;
   md_objects : Declaremods.library_objects;
@@ -135,7 +135,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module LibraryOrdered = 
+module LibraryOrdered =
   struct
     type t = dir_path
     let compare d1 d2 =
@@ -164,7 +164,7 @@ let freeze () =
   !libraries_imports_list,
   !libraries_exports_list
 
-let unfreeze (mt,mo,mi,me) = 
+let unfreeze (mt,mo,mi,me) =
   libraries_table := mt;
   libraries_loaded_list := mo;
   libraries_imports_list := mi;
@@ -176,7 +176,7 @@ let init () =
   libraries_imports_list := [];
   libraries_exports_list := []
 
-let _ = 
+let _ =
   Summary.declare_summary "MODULES"
     { Summary.freeze_function = freeze;
       Summary.unfreeze_function = unfreeze;
@@ -195,7 +195,7 @@ let try_find_library dir =
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
   (* from a previous play of the session *)
-  libraries_filename_table := 
+  libraries_filename_table :=
     LibraryFilenameMap.add dir f !libraries_filename_table
 
 let library_full_filename dir =
@@ -212,13 +212,13 @@ let library_is_loaded dir =
   try let _ = find_library dir in true
   with Not_found -> false
 
-let library_is_opened dir = 
+let library_is_opened dir =
   List.exists (fun m -> m.library_name = dir) !libraries_imports_list
 
 let library_is_exported dir =
   List.exists (fun m -> m.library_name = dir) !libraries_exports_list
 
-let loaded_libraries () = 
+let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
 
 let opened_libraries () =
@@ -249,7 +249,7 @@ let rec remember_last_of_each l m =
 
 let register_open_library export m =
   libraries_imports_list := remember_last_of_each !libraries_imports_list m;
-  if export then 
+  if export then
     libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
 (************************************************************************)
@@ -271,14 +271,14 @@ let open_library export explicit_libs m =
     Declaremods.really_import_module (MPfile m.library_name)
   end
   else
-    if export then 
+    if export then
       libraries_exports_list := remember_last_of_each !libraries_exports_list m
 
-(* open_libraries recursively open a list of libraries but opens only once 
+(* open_libraries recursively open a list of libraries but opens only once
    a library that is re-exported many times *)
 
 let open_libraries export modl =
-  let to_open_list = 
+  let to_open_list =
     List.fold_left
       (fun l m ->
          let subimport =
@@ -299,19 +299,19 @@ let open_import i (_,(dir,export)) =
     (* if not (library_is_opened dir) then *)
       open_libraries export [try_find_library dir]
 
-let cache_import obj = 
+let cache_import obj =
   open_import 1 obj
 
 let subst_import (_,_,o) = o
 
 let export_import o = Some o
 
-let classify_import (_,export as obj) = 
+let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
 
 let (in_import, out_import) =
-  declare_object {(default_object "IMPORT LIBRARY") with 
+  declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
        subst_function = subst_import;
@@ -376,7 +376,7 @@ let explain_locate_library_error qid = function
   | LibUnmappedDir ->
       let prefix, _ = repr_qualid qid in
       errorlabstrm "load_absolute_library_from"
-      (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ 
+      (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
       str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
   | LibNotFound ->
       errorlabstrm "load_absolute_library_from"
@@ -393,14 +393,14 @@ let try_locate_qualified_library (loc,qid) =
   try
     let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in
     dir,f
-  with e -> 
+  with e ->
     explain_locate_library_error qid e
 
 
 (************************************************************************)
 (* Internalise libraries *)
 
-let lighten_library m = 
+let lighten_library m =
   if !Flags.dont_load_proofs then lighten_library m else m
 
 let mk_library md digest = {
@@ -464,7 +464,7 @@ let rec_intern_by_filename_only id f =
   (* We check no other file containing same library is loaded *)
   if library_is_loaded m.library_name then
     begin
-      Flags.if_verbose warning 
+      Flags.if_verbose warning
 	((string_of_dirpath m.library_name)^" is already loaded from file "^
 	library_full_filename m.library_name);
       m.library_name, []
@@ -476,15 +476,15 @@ let rec_intern_by_filename_only id f =
 let rec_intern_library_from_file idopt f =
   (* A name is specified, we have to check it contains library id *)
   let paths = get_load_paths () in
-  let _, f = 
+  let _, f =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in
   rec_intern_by_filename_only idopt f
 
 (**********************************************************************)
-(*s [require_library] loads and possibly opens a library. This is a 
+(*s [require_library] loads and possibly opens a library. This is a
     synchronized operation. It is performed as follows:
 
-  preparation phase: (functions require_library* ) the library and its 
+  preparation phase: (functions require_library* ) the library and its
     dependencies are read from to disk (using intern_* )
     [they are read from disk to ensure that at section/module
      discharging time, the physical library referred to outside the
@@ -492,8 +492,8 @@ let rec_intern_library_from_file idopt f =
      the section/module]
 
   execution phase: (through add_leaf and cache_require)
-    the library is loaded in the environment and Nametab, the objects are 
-    registered etc, using functions from Declaremods (via load_library, 
+    the library is loaded in the environment and Nametab, the objects are
+    registered etc, using functions from Declaremods (via load_library,
     which recursively loads its dependencies)
 *)
 
@@ -501,14 +501,14 @@ type library_reference = dir_path list * bool option
 
 let register_library (dir,m) =
   Declaremods.register_library
-    m.library_name 
-    m.library_compiled 
-    m.library_objects 
+    m.library_name
+    m.library_compiled
+    m.library_objects
     m.library_digest;
   register_loaded_library m
 
 (* Follow the semantics of Anticipate object:
-   - called at module or module type closing when a Require occurs in 
+   - called at module or module type closing when a Require occurs in
      the module or module type
    - not called from a library (i.e. a module identified with a file) *)
 let load_require _ (_,(needed,modl,_)) =
@@ -529,7 +529,7 @@ let export_require (_,l,e) = Some ([],l,e)
 
 let discharge_require (_,o) = Some o
 
-(* open_function is never called from here because an Anticipate object *) 
+(* open_function is never called from here because an Anticipate object *)
 
 let (in_require, out_require) =
   declare_object {(default_object "REQUIRE") with
@@ -549,7 +549,7 @@ let set_xml_require f = xml_require := f
 let require_library_from_dirpath modrefl export =
   let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
   let modrefl = List.map fst modrefl in
-    if Lib.is_modtype () || Lib.is_module () then 
+    if Lib.is_modtype () || Lib.is_module () then
       begin
 	add_anonymous_leaf (in_require (needed,modrefl,None));
 	Option.iter (fun exp ->
@@ -583,7 +583,7 @@ let require_library_from_file idopt file export =
 let import_module export (loc,qid) =
   try
     match Nametab.locate_module qid with
-      | MPfile dir -> 
+      | MPfile dir ->
 	  if Lib.is_modtype () || Lib.is_module () || not export then
 	    add_anonymous_leaf (in_import (dir, export))
 	  else
@@ -595,7 +595,7 @@ let import_module export (loc,qid) =
 	user_err_loc
           (loc,"import_library",
 	  str ((string_of_qualid qid)^" is not a module"))
-  
+
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
@@ -606,7 +606,7 @@ let check_coq_overwriting p id =
       (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
-let start_library f = 
+let start_library f =
   let paths = get_load_paths () in
   let _,longf =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
@@ -628,15 +628,15 @@ let current_reexports () =
 
 let error_recursively_dependent_library dir =
   errorlabstrm ""
-    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ 
+    (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
 
 (* Security weakness: file might have been changed on disk between
-   writing the content and computing the checksum... *) 
+   writing the content and computing the checksum... *)
 let save_library_to dir f =
   let cenv, seg = Declaremods.end_library dir in
-  let md = { 
+  let md = {
     md_name = dir;
     md_compiled = cenv;
     md_objects = seg;
@@ -661,5 +661,5 @@ open Printf
 let mem s =
   let m = try_find_library s in
   h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)"
-		 (size_kb m) (size_kb m.library_compiled) 
+		 (size_kb m) (size_kb m.library_compiled)
 		 (size_kb m.library_objects)))