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

6 files changed, 119 insertions, 119 deletions

diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 2d4dd4a78..386ef82af 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -248,7 +248,7 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
 
 val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
   ?allow:(Gdk.Tags.modifier list) ->
-  ?f: (Gdk.Tags.modifier list -> unit) -> 
+  ?f: (Gdk.Tags.modifier list -> unit) ->
     string -> Gdk.Tags.modifier list -> parameter_kind
 
 (** [custom box f expand] creates a custom parameter, with
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 3ab3823de..ff74a3c33 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -810,13 +810,13 @@ class modifiers_param_box param =
       ()
   in
   let value = ref param.md_value in
-  let _ = 
+  let _ =
     match param.md_help with
       None -> ()
     | Some help ->
 	let tooltips = GData.tooltips () in
 	ignore (hbox#connect#destroy ~callback: tooltips#destroy);
-	tooltips#set_tip wev#coerce ~text: help ~privat: help 
+	tooltips#set_tip wev#coerce ~text: help ~privat: help
   in
   let _ = we#set_text (Configwin_types.modifiers_to_string param.md_value) in
   let mods_we_care = param.md_allow in
@@ -830,7 +830,7 @@ class modifiers_param_box param =
     we#set_text (Configwin_types.modifiers_to_string !value);
     false
   in
-  let _ = 
+  let _ =
     if param.md_editable then
       ignore (we#event#connect#key_press capture)
     else
@@ -1093,13 +1093,13 @@ let edit ?(with_apply=true)
       (fun conf_struct -> new configuration_box tooltips conf_struct wnote)
       conf_struct_list
   in
-    
+
     if with_apply then
       dialog#add_button Configwin_messages.mApply `APPLY;
-    
+
     dialog#add_button Configwin_messages.mOk `OK;
     dialog#add_button Configwin_messages.mCancel `CANCEL;
-    
+
     let f_apply () =
       List.iter (fun param_box -> param_box#apply) list_param_box  ;
       apply ()
@@ -1441,11 +1441,11 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
       hk_expand = expand ;
     }
 
-let modifiers 
-  ?(editable=true) 
-  ?(expand=true) 
-  ?help 
-  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5]) 
+let modifiers
+  ?(editable=true)
+  ?(expand=true)
+  ?help
+  ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
   ?(f=(fun _ -> ())) label v =
   Modifiers_param
     {
@@ -1456,7 +1456,7 @@ let modifiers
       md_f_apply = f ;
       md_expand = expand ;
       md_allow = allow ;
-    } 
+    }
 
 (** Create a custom param.*)
 let custom ?label box f expand =
diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index e1d7f33bb..9f44e5c6b 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -25,7 +25,7 @@
 
 (** Key codes
 
-   Ce fichier provient de X11/keysymdef.h 
+   Ce fichier provient de X11/keysymdef.h
    les noms des symboles deviennent : XK_ -> xk_
 
    Thanks to Fabrice Le Fessant.
@@ -1334,11 +1334,11 @@ let xk_Thai_khokhai					= 0xda2
 let xk_Thai_khokhuat				= 0xda3
 let xk_Thai_khokhwai				= 0xda4
 let xk_Thai_khokhon					= 0xda5
-let xk_Thai_khorakhang			        = 0xda6  
-let xk_Thai_ngongu					= 0xda7  
-let xk_Thai_chochan					= 0xda8  
-let xk_Thai_choching				= 0xda9   
-let xk_Thai_chochang				= 0xdaa  
+let xk_Thai_khorakhang			        = 0xda6
+let xk_Thai_ngongu					= 0xda7
+let xk_Thai_chochan					= 0xda8
+let xk_Thai_choching				= 0xda9
+let xk_Thai_chochang				= 0xdaa
 let xk_Thai_soso					= 0xdab
 let xk_Thai_chochoe					= 0xdac
 let xk_Thai_yoying					= 0xdad
@@ -1380,39 +1380,39 @@ let xk_Thai_saraa					= 0xdd0
 let xk_Thai_maihanakat				= 0xdd1
 let xk_Thai_saraaa					= 0xdd2
 let xk_Thai_saraam					= 0xdd3
-let xk_Thai_sarai					= 0xdd4   
-let xk_Thai_saraii					= 0xdd5   
-let xk_Thai_saraue					= 0xdd6    
-let xk_Thai_sarauee					= 0xdd7    
-let xk_Thai_sarau					= 0xdd8    
-let xk_Thai_sarauu					= 0xdd9   
+let xk_Thai_sarai					= 0xdd4
+let xk_Thai_saraii					= 0xdd5
+let xk_Thai_saraue					= 0xdd6
+let xk_Thai_sarauee					= 0xdd7
+let xk_Thai_sarau					= 0xdd8
+let xk_Thai_sarauu					= 0xdd9
 let xk_Thai_phinthu					= 0xdda
 let xk_Thai_maihanakat_maitho   			= 0xdde
 let xk_Thai_baht					= 0xddf
-let xk_Thai_sarae					= 0xde0    
+let xk_Thai_sarae					= 0xde0
 let xk_Thai_saraae					= 0xde1
 let xk_Thai_sarao					= 0xde2
-let xk_Thai_saraaimaimuan				= 0xde3   
-let xk_Thai_saraaimaimalai				= 0xde4  
+let xk_Thai_saraaimaimuan				= 0xde3
+let xk_Thai_saraaimaimalai				= 0xde4
 let xk_Thai_lakkhangyao				= 0xde5
 let xk_Thai_maiyamok				= 0xde6
 let xk_Thai_maitaikhu				= 0xde7
-let xk_Thai_maiek					= 0xde8   
+let xk_Thai_maiek					= 0xde8
 let xk_Thai_maitho					= 0xde9
 let xk_Thai_maitri					= 0xdea
 let xk_Thai_maichattawa				= 0xdeb
 let xk_Thai_thanthakhat				= 0xdec
 let xk_Thai_nikhahit				= 0xded
-let xk_Thai_leksun					= 0xdf0 
-let xk_Thai_leknung					= 0xdf1  
-let xk_Thai_leksong					= 0xdf2 
+let xk_Thai_leksun					= 0xdf0
+let xk_Thai_leknung					= 0xdf1
+let xk_Thai_leksong					= 0xdf2
 let xk_Thai_leksam					= 0xdf3
-let xk_Thai_leksi					= 0xdf4  
-let xk_Thai_lekha					= 0xdf5  
-let xk_Thai_lekhok					= 0xdf6  
-let xk_Thai_lekchet					= 0xdf7  
-let xk_Thai_lekpaet					= 0xdf8  
-let xk_Thai_lekkao					= 0xdf9 
+let xk_Thai_leksi					= 0xdf4
+let xk_Thai_lekha					= 0xdf5
+let xk_Thai_lekhok					= 0xdf6
+let xk_Thai_lekchet					= 0xdf7
+let xk_Thai_lekpaet					= 0xdf8
+let xk_Thai_lekkao					= 0xdf9
 
 
 (*
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 0def0b25d..bf2b74ee6 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -111,7 +111,7 @@ let modifiers_to_string m =
                   ) ^ s)
   in
     iter m ""
-      
+
 let value_to_key v =
   match v with
     Raw.String s -> string_to_key s
@@ -233,7 +233,7 @@ type hotkey_param = {
 
 type modifiers_param = {
     md_label : string ; (** the label of the parameter *)
-    mutable md_value : Gdk.Tags.modifier list ; 
+    mutable md_value : Gdk.Tags.modifier list ;
              (** The value, as a list of modifiers and a key code *)
     md_editable : bool ; (** indicates if the value can be changed *)
     md_f_apply : Gdk.Tags.modifier list -> unit ;
@@ -241,7 +241,7 @@ type modifiers_param = {
     md_help : string option ; (** optional help string *)
     md_expand : bool ; (** expand or not *)
     md_allow : Gdk.Tags.modifier list
-  } 
+  }
 
 
 let mk_custom_text_string_param (a : 'a string_param) : string string_param =
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 5441f4abe..1ab107c77 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -1,21 +1,21 @@
 open GTree
 open Gobject
 
-let create l = 
+let create l =
   let hbox = GPack.hbox () in
-  let scw = GBin.scrolled_window 
-	      ~hpolicy:`AUTOMATIC 
-	      ~vpolicy:`AUTOMATIC 
+  let scw = GBin.scrolled_window
+	      ~hpolicy:`AUTOMATIC
+	      ~vpolicy:`AUTOMATIC
 	      ~packing:(hbox#pack ~expand:true) () in
 
   let columns = new GTree.column_list in
   let command_col =  columns#add Data.string in
   let coq_col = columns#add Data.string in
   let store = GTree.list_store columns
-  in 
+  in
 
 (* populate the store *)
-  let _ = List.iter (fun (x,y) -> 
+  let _ = List.iter (fun (x,y) ->
 		       let row = store#append () in
 		       store#set ~row ~column:command_col x;
 		       store#set ~row ~column:coq_col y)
@@ -27,61 +27,61 @@ let create l =
   view#set_rules_hint true;
 
   let renderer_comm = GTree.cell_renderer_text [`EDITABLE true]  in
-  ignore (renderer_comm#connect#edited 
-    ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-		 store#set 
-		 ~row:(store#get_iter path) 
+  ignore (renderer_comm#connect#edited
+    ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+		 store#set
+		 ~row:(store#get_iter path)
 		 ~column:command_col s));
-  let first = 
-    GTree.view_column ~title:"Coq Command to try" 
-      ~renderer:(renderer_comm,["text",command_col]) 
-      () 
+  let first =
+    GTree.view_column ~title:"Coq Command to try"
+      ~renderer:(renderer_comm,["text",command_col])
+      ()
   in ignore (view#append_column first);
 
   let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in
   ignore(renderer_coq#connect#edited
-	   ~callback:(fun (path:Gtk.tree_path) (s:string) -> 
-			store#set 
-			~row:(store#get_iter path) 
+	   ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+			store#set
+			~row:(store#get_iter path)
 			~column:coq_col s));
-  let second = 
-    GTree.view_column ~title:"Coq Command to insert" 
-      ~renderer:(renderer_coq,["text",coq_col]) 
-      () 
+  let second =
+    GTree.view_column ~title:"Coq Command to insert"
+      ~renderer:(renderer_coq,["text",coq_col])
+      ()
   in ignore (view#append_column second);
 
-  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD () 
+  let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD ()
   in
   let up = GButton.button  ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
-  let down = GButton.button 
-	       ~stock:`GO_DOWN 
-	       ~label:"Down" 
-	       ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  let down = GButton.button
+	       ~stock:`GO_DOWN
+	       ~label:"Down"
+	       ~packing:(vbox#pack ~expand:true ~fill:false) ()
   in
-  let add = GButton.button ~stock:`ADD 
-	      ~label:"Add" 
-	      ~packing:(vbox#pack ~expand:true ~fill:false) 
-	      () 
+  let add = GButton.button ~stock:`ADD
+	      ~label:"Add"
+	      ~packing:(vbox#pack ~expand:true ~fill:false)
+	      ()
   in
-  let remove = GButton.button ~stock:`REMOVE 
-		 ~label:"Remove" 
-		 ~packing:(vbox#pack ~expand:true ~fill:false) () 
+  let remove = GButton.button ~stock:`REMOVE
+		 ~label:"Remove"
+		 ~packing:(vbox#pack ~expand:true ~fill:false) ()
   in
 
-  ignore (add#connect#clicked 
-	    ~callback:(fun b ->  
+  ignore (add#connect#clicked
+	    ~callback:(fun b ->
 			 let n = store#append () in
 			 view#selection#select_iter n));
-  ignore (remove#connect#clicked 
-	    ~callback:(fun b -> match view#selection#get_selected_rows with 
+  ignore (remove#connect#clicked
+	    ~callback:(fun b -> match view#selection#get_selected_rows with
 			 | [] -> ()
 			 | path::_ ->
 			     let iter = store#get_iter path in
 		       	     ignore (store#remove iter);
 		      ));
-  ignore (up#connect#clicked 
-	    ~callback:(fun b ->  
-			 match view#selection#get_selected_rows with 
+  ignore (up#connect#clicked
+	    ~callback:(fun b ->
+			 match view#selection#get_selected_rows with
 			   | [] -> ()
 			   | path::_ ->
 			       let iter = store#get_iter path in
@@ -89,9 +89,9 @@ let create l =
 			       let upiter = store#get_iter path in
 			       ignore (store#swap iter upiter);
 		      ));
-  ignore (down#connect#clicked 
-	    ~callback:(fun b ->  
-			 match view#selection#get_selected_rows with 
+  ignore (down#connect#clicked
+	    ~callback:(fun b ->
+			 match view#selection#get_selected_rows with
 			   | [] -> ()
 			   | path::_ ->
 			       let iter = store#get_iter path in
@@ -100,13 +100,13 @@ let create l =
 			       ignore (store#swap iter upiter)
 			       with _ -> ()
 		      ));
-  let get_data () = 
+  let get_data () =
     let start_path = GtkTree.TreePath.from_string "0" in
     let start_iter = store#get_iter start_path in
-    let rec all acc = 
+    let rec all acc =
       let new_acc = (store#get ~row:start_iter ~column:command_col,
 		     store#get ~row:start_iter ~column:coq_col)::acc
-      in      
+      in
       if store#iter_next start_iter then all new_acc else List.rev new_acc
     in all []
   in
diff --git a/ide/utils/okey.mli b/ide/utils/okey.mli
index c8d48389c..84ea4df44 100644
--- a/ide/utils/okey.mli
+++ b/ide/utils/okey.mli
@@ -23,7 +23,7 @@
 (*                                                                               *)
 (*********************************************************************************)
 
-(** Okey interface. 
+(** Okey interface.
 
    Once the lib is compiled and installed, you can use it by referencing
    it with the [Okey] module. You must add [okey.cmo] or [okey.cmx]
@@ -35,7 +35,7 @@ type modifier = Gdk.Tags.modifier
 (** Set the default modifier list. The first default value is [[]].*)
 val set_default_modifiers : modifier list -> unit
 
-(** Set the default modifier mask. The first default value is 
+(** Set the default modifier mask. The first default value is
    [[`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK]].
    The mask defines the modifiers not taken into account
    when looking for the handler of a key press event.
@@ -48,67 +48,67 @@ val set_default_mask : modifier list -> unit
    @param remove when true, the previous handlers for the given key and modifier
    list are not kept.
    @param cond this function is a guard: the [callback] function is not called
-   if the [cond] function returns [false]. 
+   if the [cond] function returns [false].
    The default [cond] function always returns [true].
 
    @param mods the list of modifiers. If not given, the default modifiers
-   are used. 
+   are used.
    You can set the default modifiers with function {!Okey.set_default_modifiers}.
 
    @param mask the list of modifiers which must not be taken
    into account to trigger the given handler. [mods]
    and [mask] must not have common modifiers. If not given, the default mask
-   is used. 
+   is used.
    You can set the default modifiers mask with function {!Okey.set_default_mask}.
 *)
 val add :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym ->
+		(unit -> unit) ->
 		  unit
 
 (** It calls {!Okey.add} for each given key.*)
-val add_list : 
+val add_list :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym list -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym list ->
+		(unit -> unit) ->
 		  unit
-	      
+
 (** Like {!Okey.add} but the previous handlers for the
    given modifiers and key are not kept.*)
 val set :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
-      event : GObj.event_ops; get_oid : int; .. > -> 
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym -> 
-		(unit -> unit) -> 
+      event : GObj.event_ops; get_oid : int; .. > ->
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym ->
+		(unit -> unit) ->
 		  unit
 
 (** It calls {!Okey.set} for each given key.*)
-val set_list : 
+val set_list :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
       event : GObj.event_ops; get_oid : int; .. > ->
-	?cond: (unit -> bool) -> 
-	  ?mods: modifier list -> 
-	    ?mask: modifier list -> 
-	      Gdk.keysym list -> 
-		(unit -> unit) -> 
+	?cond: (unit -> bool) ->
+	  ?mods: modifier list ->
+	    ?mask: modifier list ->
+	      Gdk.keysym list ->
+		(unit -> unit) ->
 		  unit
 
 (** Remove the handlers associated to the given widget.
    This is automatically done when a widget is destroyed but
    you can do it yourself. *)
-val remove_widget : 
+val remove_widget :
     < connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
       event : GObj.event_ops; get_oid : int; .. > ->
 	unit ->