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, 25 insertions, 25 deletions

diff --git a/library/libobject.ml b/library/libobject.ml
index 504c1ffdd..95894294b 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -25,7 +25,7 @@ let relax_flag = ref false;;
 
 let relax b = relax_flag := b;;
 
-type 'a substitutivity = 
+type 'a substitutivity =
     Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a
 
 type 'a object_declaration = {
@@ -46,12 +46,12 @@ let default_object s = {
   cache_function = (fun _ -> ());
   load_function = (fun _ _ -> ());
   open_function = (fun _ _ -> ());
-  subst_function = (fun _ -> 
+  subst_function = (fun _ ->
     yell ("The object "^s^" does not know how to substitute!"));
   classify_function = (fun obj -> Keep obj);
   discharge_function = (fun _ -> None);
   rebuild_function = (fun x -> x);
-  export_function = (fun _ -> None)} 
+  export_function = (fun _ -> None)}
 
 
 (* The suggested object declaration is the following:
@@ -59,7 +59,7 @@ let default_object s = {
    declare_object { (default_object "MY OBJECT") with
        cache_function = fun (sp,a) -> Mytbl.add sp a}
 
-   and the listed functions are only those which definitions accually 
+   and the listed functions are only those which definitions accually
    differ from the default.
 
    This helps introducing new functions in objects.
@@ -81,7 +81,7 @@ type dynamic_object_declaration = {
 
 let object_tag lobj = Dyn.tag lobj
 
-let cache_tab = 
+let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
 let declare_object odecl =
@@ -96,34 +96,34 @@ let declare_object odecl =
   and opener i (oname,lobj) =
     if Dyn.tag lobj = na then odecl.open_function i (oname,outfun lobj)
     else anomaly "somehow we got the wrong dynamic object in the openfun"
-  and substituter (oname,sub,lobj) = 
-    if Dyn.tag lobj = na then 
+  and substituter (oname,sub,lobj) =
+    if Dyn.tag lobj = na then
       infun (odecl.subst_function (oname,sub,outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the substfun"
-  and classifier lobj = 
-    if Dyn.tag lobj = na then 
+  and classifier lobj =
+    if Dyn.tag lobj = na then
       match odecl.classify_function (outfun lobj) with
 	| Dispose -> Dispose
 	| Substitute obj -> Substitute (infun obj)
 	| Keep obj -> Keep (infun obj)
 	| Anticipate (obj) -> Anticipate (infun obj)
-    else 
+    else
       anomaly "somehow we got the wrong dynamic object in the classifyfun"
-  and discharge (oname,lobj) = 
-    if Dyn.tag lobj = na then 
+  and discharge (oname,lobj) =
+    if Dyn.tag lobj = na then
       Option.map infun (odecl.discharge_function (oname,outfun lobj))
-    else 
+    else
       anomaly "somehow we got the wrong dynamic object in the dischargefun"
-  and rebuild lobj = 
+  and rebuild lobj =
     if Dyn.tag lobj = na then infun (odecl.rebuild_function (outfun lobj))
     else anomaly "somehow we got the wrong dynamic object in the rebuildfun"
-  and exporter lobj = 
-    if Dyn.tag lobj = na then 
+  and exporter lobj =
+    if Dyn.tag lobj = na then
       Option.map infun (odecl.export_function (outfun lobj))
-    else 
+    else
       anomaly "somehow we got the wrong dynamic object in the exportfun"
 
-  in 
+  in
   Hashtbl.add cache_tab na { dyn_cache_function = cacher;
 			     dyn_load_function = loader;
                              dyn_open_function = opener;
@@ -144,13 +144,13 @@ let apply_dyn_fun deflt f lobj =
       let dodecl =
     	try
 	  Hashtbl.find cache_tab tag
-    	with Not_found -> 
+    	with Not_found ->
 	  if !relax_flag then
 	    failwith "local to_apply_dyn_fun"
 	  else
 	    error
 	      ("Cannot find library functions for an object with tag "^tag^
-	       " (maybe a plugin is missing)") in 
+	       " (maybe a plugin is missing)") in
 	f dodecl
     with
 	Failure "local to_apply_dyn_fun" -> deflt;;
@@ -158,19 +158,19 @@ let apply_dyn_fun deflt f lobj =
 let cache_object ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj
 
-let load_object i ((_,lobj) as node) = 
+let load_object i ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj
 
-let open_object i ((_,lobj) as node) = 
+let open_object i ((_,lobj) as node) =
   apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj
 
-let subst_object ((_,_,lobj) as node) = 
+let subst_object ((_,_,lobj) as node) =
   apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj
 
-let classify_object lobj = 
+let classify_object lobj =
   apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj
 
-let discharge_object ((_,lobj) as node) = 
+let discharge_object ((_,lobj) as node) =
   apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj
 
 let rebuild_object lobj =