[coq] Untabify the whole ML codebase.

We also remove trailing whitespace.

Script used:

```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```

18 files changed, 235 insertions, 235 deletions

diff --git a/ide/configwin.mli b/ide/configwin.mli
index fa22846d19..b5c3e74aec 100644
--- a/ide/configwin.mli
+++ b/ide/configwin.mli
@@ -42,13 +42,13 @@ type configuration_structure =
 type return_button =
     Return_apply
       (** The user clicked on Apply at least once before
-	 closing the window with Cancel or the window manager. *)
+         closing the window with Cancel or the window manager. *)
   | Return_ok
       (** The user closed the window with the ok button. *)
   | Return_cancel
       (** The user closed the window with the cancel
-	 button or the window manager but never clicked
-	 on the apply button.*)
+         button or the window manager but never clicked
+         on the apply button.*)
 
 (** {2 Functions to create parameters} *)
 
@@ -84,7 +84,7 @@ val strings : ?editable: bool -> ?help: string ->
   ?f: (string list -> unit) ->
     ?eq: (string -> string -> bool) ->
       ?add: (unit -> string list) ->
-	string -> string list -> parameter_kind
+        string -> string list -> parameter_kind
 
 (** [list label f_strings value] creates a list parameter.
    [f_strings] is a function taking a value and returning a list
@@ -113,13 +113,13 @@ val list : ?editable: bool -> ?help: string ->
   ?f: ('a list -> unit) ->
     ?eq: ('a -> 'a -> bool) ->
       ?edit: ('a -> 'a) ->
-	?add: (unit -> 'a list) ->
-	  ?titles: string list ->
-	    ?color: ('a -> string option) ->
-	      string ->
-		('a -> string list) ->
-		  'a list ->
-		    parameter_kind
+        ?add: (unit -> 'a list) ->
+          ?titles: string list ->
+            ?color: ('a -> string option) ->
+              string ->
+                ('a -> string list) ->
+                  'a list ->
+                    parameter_kind
 *)
 
 (** [combo label choices value] creates a combo parameter.
diff --git a/ide/configwin_ihm.ml b/ide/configwin_ihm.ml
index 0f3fd38a7a..e768131dcf 100644
--- a/ide/configwin_ihm.ml
+++ b/ide/configwin_ihm.ml
@@ -38,15 +38,15 @@ let modifiers_to_string m =
       | c :: m ->
           iter m ((
                     match c with
-			`CONTROL -> "<ctrl>"
-		      | `SHIFT -> "<shft>"
-		      | `LOCK -> "<lock>"
-		      | `MOD1 -> "<alt>"
-		      | `MOD2 -> "<mod2>"
-		      | `MOD3 -> "<mod3>"
-		      | `MOD4 -> "<mod4>"
-		      | `MOD5 -> "<mod5>"
-		      | _  -> raise Not_found
+                        `CONTROL -> "<ctrl>"
+                      | `SHIFT -> "<shft>"
+                      | `LOCK -> "<lock>"
+                      | `MOD1 -> "<alt>"
+                      | `MOD2 -> "<mod2>"
+                      | `MOD3 -> "<mod3>"
+                      | `MOD4 -> "<mod4>"
+                      | `MOD5 -> "<mod5>"
+                      | _  -> raise Not_found
                   ) ^ s)
   in
     iter m ""
@@ -89,13 +89,13 @@ class ['a] list_selection_box
   let wlist = match titles_opt with
     None ->
       GList.clist ~selection_mode: `MULTIPLE
-	~titles_show: false
-	~packing: wscroll#add ()
+        ~titles_show: false
+        ~packing: wscroll#add ()
   | Some l ->
       GList.clist ~selection_mode: `MULTIPLE
-	~titles: l
-	~titles_show: true
-	~packing: wscroll#add ()
+        ~titles: l
+        ~titles_show: true
+        ~packing: wscroll#add ()
   in
   let _ = set_help_tip wev help_opt in
   (* the vbox for the buttons *)
@@ -146,18 +146,18 @@ class ['a] list_selection_box
       wlist#freeze ();
       wlist#clear ();
       List.iter
-	(fun ele ->
-	  ignore (wlist#append (f_strings ele));
-	  match f_color ele with
-	    None -> ()
-	  | Some c ->
-	      try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1)
-	      with _ -> ()
-	)
-	!listref;
+        (fun ele ->
+          ignore (wlist#append (f_strings ele));
+          match f_color ele with
+            None -> ()
+          | Some c ->
+              try wlist#set_row ~foreground: (`NAME c) (wlist#rows - 1)
+              with _ -> ()
+        )
+        !listref;
 
       (match titles_opt with
-	None -> wlist#columns_autosize ()
+        None -> wlist#columns_autosize ()
       |	Some _ -> GToolbox.autosize_clist wlist);
       wlist#thaw ();
       (* the list of selectd elements is now empty *)
@@ -166,18 +166,18 @@ class ['a] list_selection_box
     (** Move up the selected rows. *)
     method up_selected =
       let rec iter n selrows l =
-	match selrows with
-	  [] -> (l, [])
-	| m :: qrows ->
-	    match l with
-	      [] -> ([],[])
-	    | [_] -> (l,[])
-	    | e1 :: e2 :: q when m = n + 1 ->
-		let newl, newrows = iter (n+1) qrows (e1 :: q) in
-		(e2 :: newl, n :: newrows)
-	    | e1 :: q ->
-		let newl, newrows = iter (n+1) selrows q in
-		(e1 ::  newl, newrows)
+        match selrows with
+          [] -> (l, [])
+        | m :: qrows ->
+            match l with
+              [] -> ([],[])
+            | [_] -> (l,[])
+            | e1 :: e2 :: q when m = n + 1 ->
+                let newl, newrows = iter (n+1) qrows (e1 :: q) in
+                (e2 :: newl, n :: newrows)
+            | e1 :: q ->
+                let newl, newrows = iter (n+1) selrows q in
+                (e1 ::  newl, newrows)
       in
       let sorted_select = List.sort compare list_select in
       let new_list, new_rows = iter 0 sorted_select !listref in
@@ -188,24 +188,24 @@ class ['a] list_selection_box
     method edit_selected f_edit =
       let sorted_select = List.sort compare list_select in
       match sorted_select with
-	[] -> ()
+        [] -> ()
       |	n :: _ ->
-	  try
-	    let ele = List.nth !listref n in
-	    let ele2 = f_edit ele in
-	    let rec iter m = function
-		[] -> []
-	      |	e :: q ->
-		  if n = m then
-		    ele2 :: q
-		  else
-		    e :: (iter (m+1) q)
-	    in
-	    self#update (iter 0 !listref);
-	    wlist#select n 0
-	  with
-	    Not_found ->
-	      ()
+          try
+            let ele = List.nth !listref n in
+            let ele2 = f_edit ele in
+            let rec iter m = function
+                [] -> []
+              |	e :: q ->
+                  if n = m then
+                    ele2 :: q
+                  else
+                    e :: (iter (m+1) q)
+            in
+            self#update (iter 0 !listref);
+            wlist#select n 0
+          with
+            Not_found ->
+              ()
 
     initializer
 
@@ -228,14 +228,14 @@ class ['a] list_selection_box
       in
       let f_remove () =
         (* remove the selected items from the listref and the clist *)
-	let rec iter n = function
-	    [] -> []
-	  | h :: q ->
-	      if List.mem n list_select then
-		iter (n+1) q
-	      else
-		h :: (iter (n+1) q)
-	in
+        let rec iter n = function
+            [] -> []
+          | h :: q ->
+              if List.mem n list_select then
+                iter (n+1) q
+              else
+                h :: (iter (n+1) q)
+        in
         let new_list = iter 0 !listref in
         self#update new_list
       in
@@ -248,10 +248,10 @@ class ['a] list_selection_box
       ignore (wb_up#connect#clicked ~callback:(fun () -> self#up_selected));
       (
        match f_edit_opt with
-	 None -> ()
+         None -> ()
        | Some f ->
-	   let _ = dbg "list_selection_box: connecting wb_edit" in
-	   ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f))
+           let _ = dbg "list_selection_box: connecting wb_edit" in
+           ignore (wb_edit#connect#clicked ~callback:(fun () -> self#edit_selected f))
       );
       (* connect the selection and deselection of items in the clist *)
       let f_select ~row ~column ~event =
@@ -303,10 +303,10 @@ class string_param_box param =
     method apply =
       let new_value = param.string_of_string we#text in
       if new_value <> param.string_value then
-	let _ = param.string_f_apply new_value in
-	param.string_value <- new_value
+        let _ = param.string_f_apply new_value in
+        param.string_value <- new_value
       else
-	()
+        ()
   end ;;
 
 (** This class is used to build a box for a combo parameter.*)
@@ -318,16 +318,16 @@ class combo_param_box param =
     let _ = set_help_tip wev param.combo_help in
     let get_value = if not param.combo_new_allowed then
       let wc = GEdit.combo_box_text
-	~strings: param.combo_choices
-	?active:(let rec aux i = function
-		   |[] -> None
-		   |h::_ when h = param.combo_value -> Some i
-		   |_::t -> aux (succ i) t
-		 in aux 0 param.combo_choices)
-	~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
-	()
+        ~strings: param.combo_choices
+        ?active:(let rec aux i = function
+                   |[] -> None
+                   |h::_ when h = param.combo_value -> Some i
+                   |_::t -> aux (succ i) t
+                 in aux 0 param.combo_choices)
+        ~packing: (hbox#pack ~expand: param.combo_expand ~padding: 2)
+        ()
       in
-	fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
+        fun () -> match GEdit.text_combo_get_active wc with |None -> "" |Some s -> s
     else
       let (wc,_) = GEdit.combo_box_entry_text
        ~strings: param.combo_choices
@@ -347,10 +347,10 @@ object (self)
   method apply =
     let new_value = get_value () in
       if new_value <> param.combo_value then
-	let _ = param.combo_f_apply new_value in
-	  param.combo_value <- new_value
+        let _ = param.combo_f_apply new_value in
+          param.combo_value <- new_value
       else
-	()
+        ()
 end ;;
 
 (** Class used to pack a custom box. *)
@@ -360,9 +360,9 @@ class custom_param_box param =
     match param.custom_framed with
       None -> param.custom_box#coerce
     | Some l ->
-	let wf = GBin.frame ~label: l () in
-	wf#add param.custom_box#coerce;
-	wf#coerce
+        let wf = GBin.frame ~label: l () in
+        wf#add param.custom_box#coerce;
+        wf#coerce
   in
   object (self)
     method box = top
@@ -401,13 +401,13 @@ class text_param_box param =
     method apply =
       let v = param.string_of_string (buffer#get_text ()) in
       if v <> param.string_value then
-	(
-	 dbg "apply new value!";
-	 let _ = param.string_f_apply v in
-	 param.string_value <- v
-	)
+        (
+         dbg "apply new value!";
+         let _ = param.string_f_apply v in
+         param.string_value <- v
+        )
       else
-	()
+        ()
   end ;;
 
 (** This class is used to build a box for a boolean parameter.*)
@@ -430,10 +430,10 @@ class bool_param_box param =
     method apply =
       let new_value = wchk#active in
       if new_value <> param.bool_value then
-	let _ = param.bool_f_apply new_value in
-	param.bool_value <- new_value
+        let _ = param.bool_f_apply new_value in
+        param.bool_value <- new_value
       else
-	()
+        ()
   end ;;
 
 class modifiers_param_box param =
@@ -461,10 +461,10 @@ class modifiers_param_box param =
     method apply =
       let new_value = !value in
       if new_value <> param.md_value then
-	let _ = param.md_f_apply new_value in
-	param.md_value <- new_value
+        let _ = param.md_f_apply new_value in
+        param.md_value <- new_value
       else
-	()
+        ()
   end ;;
 (*
 (** This class is used to build a box for a parameter whose values are a list.*)
@@ -728,20 +728,20 @@ let list ?(editable=true) ?help
     label (f_strings : 'a -> string list) v =
   List_param
     (fun () ->
-	new list_param_box
-	  {
-	    list_label = label ;
-	    list_help = help ;
-	    list_value = v ;
-	    list_editable = editable ;
-	    list_titles = titles;
-	    list_eq = eq ;
-	    list_strings = f_strings ;
-	    list_color = color ;
-	    list_f_edit = edit ;
-	    list_f_add = add ;
-	    list_f_apply = f ;
-	  }
+        new list_param_box
+          {
+            list_label = label ;
+            list_help = help ;
+            list_value = v ;
+            list_editable = editable ;
+            list_titles = titles;
+            list_eq = eq ;
+            list_strings = f_strings ;
+            list_color = color ;
+            list_f_edit = edit ;
+            list_f_add = add ;
+            list_f_apply = f ;
+          }
     )
 
 (** Create a strings param. *)
@@ -818,10 +818,10 @@ let question_box ~title ~buttons ?(default=1) ?icon ?parent message =
         in
         ignore (b#connect#clicked ~callback:
           (fun () -> button_nb := n; window#destroy ()));
-	(* If it's the first button then give it the focus *)
+        (* If it's the first button then give it the focus *)
         if n = default then b#grab_default () else ();
 
-	iter_buttons (n+1) q
+        iter_buttons (n+1) q
   in
   iter_buttons 1 buttons;
   ignore (window#connect#destroy ~callback: GMain.Main.quit);
diff --git a/ide/configwin_types.ml b/ide/configwin_types.ml
index 4c66a6944e..711eccd08e 100644
--- a/ide/configwin_types.ml
+++ b/ide/configwin_types.ml
@@ -114,8 +114,8 @@ type configuration_structure =
 (** To indicate what button was pushed by the user when the window is closed. *)
 type return_button =
     Return_apply (** The user clicked on Apply at least once before
-	     closing the window with Cancel or the window manager. *)
+             closing the window with Cancel or the window manager. *)
   | Return_ok (** The user closed the window with the ok button. *)
   | Return_cancel (** The user closed the window with the cancel
-		     button or the window manager but never clicked
-		     on the apply button.*)
+                     button or the window manager but never clicked
+                     on the apply button.*)
diff --git a/ide/coq.ml b/ide/coq.ml
index 889cc3be36..4d6ba55d76 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -56,7 +56,7 @@ let rec read_all_lines in_chan =
     let len = String.length arg  in
     let arg =
       if len > 0 && arg.[len - 1] = '\r' then
-	String.sub arg 0 (len - 1)
+        String.sub arg 0 (len - 1)
       else arg
     in
     arg::(read_all_lines in_chan)
@@ -135,7 +135,7 @@ and asks_for_coqtop args =
       match file with
       | Some _ ->
           let () = custom_coqtop := file in
-	  filter_coq_opts args
+          filter_coq_opts args
       | None -> exit 0
 
 exception WrongExitStatus of string
@@ -597,8 +597,8 @@ struct
     let opts = Hashtbl.fold mkopt current_state [] in
     eval_call (Xmlprotocol.set_options opts) h
       (function
-	| Interface.Good () -> k ()
-	| _ -> failwith "Cannot set options. Resetting coqtop")
+        | Interface.Good () -> k ()
+        | _ -> failwith "Cannot set options. Resetting coqtop")
 
 end
 
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index d52f038f1f..89425bda56 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -280,7 +280,7 @@ object(self)
               List.exists (fun m ->
                 Gobject.get_oid m =
                 Gobject.get_oid (buffer#get_mark s.start)) marks in
-            try Doc.find document mem_marks 
+            try Doc.find document mem_marks
             with Not_found -> aux iter#backward_char in
         aux iter in
       let ss =
@@ -293,7 +293,7 @@ object(self)
       script#misc#set_tooltip_text ""; script#misc#set_has_tooltip true
     end;
     false
-    
+
   method destroy () =
     feedback_timer.Ideutils.kill ()
 
@@ -323,7 +323,7 @@ object(self)
 
   method private get_start_of_input =
     buffer#get_iter_at_mark (`NAME "start_of_input")
-  
+
   method private get_end_of_input =
     buffer#get_iter_at_mark (`NAME "stop_of_input")
 
@@ -697,7 +697,7 @@ object(self)
   method private find_id until =
     try
       Doc.find_id document (fun id { start;stop } -> until (Some id) start stop)
-    with Not_found -> initial_state, Doc.focused document 
+    with Not_found -> initial_state, Doc.focused document
 
   method private cleanup seg =
     if seg <> [] then begin
@@ -758,7 +758,7 @@ object(self)
                  (Doc.focused document && Doc.is_in_focus document safe_id))
     in
       undo to_id unfocus_needed)
-  
+
   method private backtrack_until ?move_insert until =
     self#backtrack_to_id ?move_insert (self#find_id until)
 
@@ -782,7 +782,7 @@ object(self)
 
   method backtrack_last_phrase =
     messages#default_route#clear;
-    try 
+    try
       let tgt = Doc.before_tip document in
       self#backtrack_to_id tgt
     with Not_found -> Coq.return (Coq.reset_coqtop _ct)
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 1e8d87bb15..58d69c0aaa 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -32,7 +32,7 @@ object
 
 
   method handle_failure : handle_exn_rty -> unit task
-  
+
   method destroy : unit -> unit
 end
 
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 14cd87e7b5..fc30690544 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -166,7 +166,7 @@ let load_file ?(maycreate=false) f =
       | [] -> false
       | sn :: sessions ->
         match sn.fileops#filename with
-	  | Some fn when is_f fn -> notebook#goto_page i; true
+          | Some fn when is_f fn -> notebook#goto_page i; true
           | _ -> search_f (i+1) sessions
     in
     if not (search_f 0 notebook#pages) then begin
@@ -257,7 +257,7 @@ let crash_save exitcode =
     in
     try
       if try_export filename (sn.buffer#get_text ()) then
-	Minilib.log ("Saved "^filename)
+        Minilib.log ("Saved "^filename)
       else Minilib.log ("Could not save "^filename)
     with _ -> Minilib.log ("Could not save "^filename)
   in
@@ -461,8 +461,8 @@ let compile sn =
     |Some f ->
       let args = Coq.get_arguments sn.coqtop in
       let cmd = cmd_coqc#get
-	^ " " ^ String.concat " " args
-	^ " " ^ (Filename.quote f) ^ " 2>&1"
+        ^ " " ^ String.concat " " args
+        ^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
       let buf = Buffer.create 1024 in
       sn.messages#default_route#set (Pp.str ("Running: "^cmd));
@@ -1040,7 +1040,7 @@ let build_ui () =
     item "Preferences" ~accel:"<Primary>comma" ~stock:`PREFERENCES
       ~callback:(fun _ ->
         begin
-	  try Preferences.configure ~apply:refresh_notebook_pos w
+          try Preferences.configure ~apply:refresh_notebook_pos w
           with e ->
             flash_info ("Editing preferences failed (" ^ Printexc.to_string e ^ ")")
         end;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 452808490d..f056af6703 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -7,14 +7,14 @@ let list_items menu li =
   let tactic_item = function
     |[] -> Buffer.create 1
     |[s] -> let b = Buffer.create 16 in
-	    let () = Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under s)^"' />\n") in
-	    b
+            let () = Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under s)^"' />\n") in
+            b
     |s::_ as l -> let b = Buffer.create 50 in
-		  let () = (Buffer.add_string b ("<menu action='"^menu^" "^(String.make 1 s.[0])^"'>\n")) in
-		  let () = (List.iter
-			     (fun x -> Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under x)^"' />\n")) l) in
-		  let () = Buffer.add_string b"</menu>\n" in
-		  b in
+                  let () = (Buffer.add_string b ("<menu action='"^menu^" "^(String.make 1 s.[0])^"'>\n")) in
+                  let () = (List.iter
+                             (fun x -> Buffer.add_string b ("<menuitem action='"^menu^" "^(no_under x)^"' />\n")) l) in
+                  let () = Buffer.add_string b"</menu>\n" in
+                  b in
   let () = List.iter (fun b -> Buffer.add_buffer res_buf (tactic_item b)) li in
   res_buf
 
diff --git a/ide/document.ml b/ide/document.ml
index cee490861d..b8e8182ab2 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -64,7 +64,7 @@ let tip = function
   | { stack = [] } -> raise Empty
   | { stack = { state_id = Some id }::_ } -> id
   | { stack = { state_id = None }::_ } -> invalid_arg "tip"
-  
+
 let tip_data = function
   | { stack = [] } -> raise Empty
   | { stack = { data }::_ } -> data
@@ -89,19 +89,19 @@ let focus d ~cond_top:c_start ~cond_bot:c_stop =
         else aux (x::a,s,b) grab xs
     | { state_id = Some id; data } as x :: xs ->
         if c_stop id data then List.rev a, List.rev (x::s), xs
-        else aux (a,x::s,b) grab xs 
+        else aux (a,x::s,b) grab xs
     | _ -> assert false in
   let a, s, b = aux ([],[],[]) false d.stack in
   d.stack <- s;
   d.context <- Some (a, b)
-  
+
 let unfocus = function
   | { context = None } -> invalid_arg "unfocus"
   | { context = Some (a,b); stack } as d ->
        assert(invariant stack);
        d.context <- None;
        d.stack <- a @ stack @ b
-  
+
 let focused { context } = context <> None
 
 let to_lists = function
@@ -117,17 +117,17 @@ let find d f =
   try List.find (flat f true)  s with Not_found ->
       List.find (flat f false) b
   ).data
-  
+
 let find_map d f =
   let a, s, b = to_lists d in
-  try CList.find_map (flat f false) a with Not_found -> 
-  try CList.find_map (flat f true)  s with Not_found -> 
+  try CList.find_map (flat f false) a with Not_found ->
+  try CList.find_map (flat f true)  s with Not_found ->
       CList.find_map (flat f false) b
-  
+
 let is_empty = function
   | { stack = []; context = None } -> true
   | _ -> false
-  
+
 let context d =
   let top, _, bot = to_lists d in
   let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
diff --git a/ide/document.mli b/ide/document.mli
index eea250bd50..c0cc848bd7 100644
--- a/ide/document.mli
+++ b/ide/document.mli
@@ -11,7 +11,7 @@
 (* An 'a document is a structure to hold and manipulate list of sentences.
    Sentences are equipped with an id = Stateid.t and can carry arbitrary
    data ('a).
-   
+
    When added (push) to the document, a sentence has no id, it has
    be manually assigned just afterward or the sentence has to be removed
    (pop) before any other sentence can be pushed.
@@ -21,7 +21,7 @@
    sentence in question, and it is simpler if the sentence is in the document.
    Only the functions pop, find, fold_all and find_map can be called on a
    document with a tip that has no id (and assign_tip_id of course).
-   
+
    The document can be focused (non recursively) to a zone.  After that
    some functions operate on the focused zone only.  When unfocused the
    context (the part of the document out of focus) is restored.
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 4b156065f3..1cf065cf25 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -18,8 +18,8 @@ let warn_image () =
   img#set_icon_size `DIALOG;
   img
 
-let warning msg = 
-   GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg 
+let warning msg =
+   GToolbox.message_box ~title:"Warning" ~icon:(warn_image ())#coerce msg
 
 let cb = GData.clipboard Gdk.Atom.primary
 
@@ -212,15 +212,15 @@ let try_export file_name s =
     try match encoding#get with
       |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s
       |Elocale ->
-	let is_unicode,char_set = Glib.Convert.get_charset () in
-	if is_unicode then
-	  (Minilib.log "Locale is UTF-8" ; s)
-	else
-	  (Minilib.log ("Locale is "^char_set);
-	   Glib.Convert.convert_with_fallback
+        let is_unicode,char_set = Glib.Convert.get_charset () in
+        if is_unicode then
+          (Minilib.log "Locale is UTF-8" ; s)
+        else
+          (Minilib.log ("Locale is "^char_set);
+           Glib.Convert.convert_with_fallback
              ~from_codeset:"UTF-8" ~to_codeset:char_set s)
       |Emanual enc ->
-	(Minilib.log ("Manual charset is "^ enc);
+        (Minilib.log ("Manual charset is "^ enc);
          Glib.Convert.convert_with_fallback
            ~from_codeset:"UTF-8" ~to_codeset:enc s)
     with e ->
@@ -279,9 +279,9 @@ let select_file_for_open ~title ?(filter=true) ?parent ?filename () =
     match file_chooser#run () with
     | `OPEN ->
       begin
-	match file_chooser#filename with
-	  | None -> None
-	  | Some _ as f ->
+        match file_chooser#filename with
+          | None -> None
+          | Some _ as f ->
             project_path#set file_chooser#current_folder; f
       end
     | `DELETE_EVENT | `CANCEL -> None in
@@ -365,12 +365,12 @@ let coqtop_path () =
             if Sys.file_exists new_prog ||
                CString.equal Filename.(basename new_prog) new_prog
             then new_prog
-	    else
-	      let in_macos_bundle =
-		Filename.concat
-		  (Filename.dirname new_prog)
-		  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
-	      in if Sys.file_exists in_macos_bundle then in_macos_bundle
+            else
+              let in_macos_bundle =
+                Filename.concat
+                  (Filename.dirname new_prog)
+                  (Filename.concat "../Resources/bin" (Filename.basename new_prog))
+              in if Sys.file_exists in_macos_bundle then in_macos_bundle
                  else "coqidetop.opt"
         with Not_found -> "coqidetop.opt"
   in file
diff --git a/ide/microPG.ml b/ide/microPG.ml
index 7d8fd44a75..9492f1a77f 100644
--- a/ide/microPG.ml
+++ b/ide/microPG.ml
@@ -153,7 +153,7 @@ let run key gui action status =
       else (b#place_cursor ~where; script#scroll_mark_onscreen `INSERT);
       status
 
-let emacs = empty 
+let emacs = empty
 
 let emacs = insert emacs "Emacs" [] [
   (* motion *)
@@ -214,7 +214,7 @@ let emacs = insert emacs "Emacs" [] [
     let k =
       if i#ends_line then begin
         b#delete ~start:i ~stop:i#forward_char; "\n"
-      end else begin 
+      end else begin
         let k = b#get_text ~start:i ~stop:i#forward_to_line_end () in
         b#delete ~start:i ~stop:i#forward_to_line_end; k
       end in
@@ -265,7 +265,7 @@ let emacs = insert emacs "Emacs" [mC,_x,"x"] [
   mkE _f "f" "Open" (Action("File", "Open"));
   mkE ~mods:[] _u "u" "Undo" (Action("Edit", "Undo"));
   ]
-  
+
 let pg = insert emacs "Proof General" [mC,_c,"c"] [
   mkE _Return "RET" "Go to" (Action("Navigation", "Go to"));
   mkE _n "n" "Advance 1 sentence" (Action("Navigation", "Forward"));
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 7b667027fc..4ee5669877 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -735,13 +735,13 @@ let configure ?(apply=(fun () -> ())) parent =
       "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
     box#pack ~expand:true w#coerce;
     ignore (w#misc#connect#realize
-	      ~callback:(fun () -> w#set_font_name text_font#get));
+              ~callback:(fun () -> w#set_font_name text_font#get));
     custom
       ~label:"Fonts for text"
       box
       (fun () ->
-	 let fd =  w#font_name in
-	 text_font#set fd)
+         let fd =  w#font_name in
+         text_font#set fd)
       true
   in
 
@@ -863,7 +863,7 @@ let configure ?(apply=(fun () -> ())) parent =
   let global_auto_revert_delay =
     string
     ~f:(fun s -> global_auto_revert_delay#set
-	  (try int_of_string s with _ -> 10000))
+          (try int_of_string s with _ -> 10000))
       "Global auto revert delay (ms)"
       (string_of_int global_auto_revert_delay#get)
   in
@@ -872,7 +872,7 @@ let configure ?(apply=(fun () -> ())) parent =
   let auto_save_delay =
     string
     ~f:(fun s -> auto_save_delay#set
-	  (try int_of_string s with _ -> 10000))
+          (try int_of_string s with _ -> 10000))
       "Auto save delay (ms)"
       (string_of_int auto_save_delay#get)
   in
@@ -891,8 +891,8 @@ let configure ?(apply=(fun () -> ())) parent =
       ~f:(fun s -> encoding#set (inputenc_of_string s))
       ~new_allowed: true
       ("UTF-8"::"LOCALE":: match encoding#get with
-	|Emanual s -> [s]
-	|_ -> []
+        |Emanual s -> [s]
+        |_ -> []
       )
       (string_of_inputenc encoding#get)
   in
@@ -1018,26 +1018,26 @@ let configure ?(apply=(fun () -> ())) parent =
    (shame on Benjamin) *)
   let cmds =
     [Section("Fonts", Some `SELECT_FONT,
-	     [config_font]);
+             [config_font]);
      Section("Colors", Some `SELECT_COLOR,
              [config_color; source_language; source_style]);
      Section("Tags", Some `SELECT_COLOR,
              [config_tags]);
      Section("Editor", Some `EDIT, [config_editor]);
      Section("Files", Some `DIRECTORY,
-	     [global_auto_revert;global_auto_revert_delay;
-	      auto_save; auto_save_delay; (* auto_save_name*)
-	      encodings; line_ending;
-	     ]);
+             [global_auto_revert;global_auto_revert_delay;
+              auto_save; auto_save_delay; (* auto_save_name*)
+              encodings; line_ending;
+             ]);
      Section("Project", Some (`STOCK "gtk-page-setup"),
-	     [project_file_name;read_project;
-	     ]);
+             [project_file_name;read_project;
+             ]);
      Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
      Section("Externals", None,
-	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
+             [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
               cmd_print;cmd_editor;cmd_browse]);
      Section("Shortcuts", Some `PREFERENCES,
-	     [modifiers_valid; modifier_for_tactics;
+             [modifiers_valid; modifier_for_tactics;
         modifier_for_templates; modifier_for_display; modifier_for_navigation;
         modifier_for_queries (*; user_queries *)]);
      Section("Misc", Some `ADD,
diff --git a/ide/protocol/xml_lexer.mli b/ide/protocol/xml_lexer.mli
index e61cb055f7..920de9f9c3 100644
--- a/ide/protocol/xml_lexer.mli
+++ b/ide/protocol/xml_lexer.mli
@@ -18,26 +18,26 @@
  *)
 
 type error =
-	| EUnterminatedComment
-	| EUnterminatedString
-	| EIdentExpected
-	| ECloseExpected
-	| ENodeExpected
-	| EAttributeNameExpected
-	| EAttributeValueExpected
-	| EUnterminatedEntity
+        | EUnterminatedComment
+        | EUnterminatedString
+        | EIdentExpected
+        | ECloseExpected
+        | ENodeExpected
+        | EAttributeNameExpected
+        | EAttributeValueExpected
+        | EUnterminatedEntity
 
 exception Error of error
 
 type token =
-	| Tag of string * (string * string) list * bool
-	| PCData of string
-	| Endtag of string
-	| Eof
+        | Tag of string * (string * string) list * bool
+        | PCData of string
+        | Endtag of string
+        | Eof
 
 type pos = int * int * int * int
 
-val init : Lexing.lexbuf -> unit 
+val init : Lexing.lexbuf -> unit
 val close : unit -> unit
 val token : Lexing.lexbuf -> token
 val pos : Lexing.lexbuf -> pos
diff --git a/ide/session.ml b/ide/session.ml
index 2824530c43..547c9814ff 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -149,7 +149,7 @@ let set_buffer_handlers
     let rec aux old it =
       if it#is_start then None
       else if it#has_tag Tags.Script.processed then Some old
-      else if it#has_tag Tags.Script.error_bg then aux it it#backward_char 
+      else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
       else None in
     aux it it in
   let insert_cb it s = if String.length s = 0 then () else begin
@@ -207,8 +207,8 @@ let set_buffer_handlers
          to a point indicated by coq. *)
       if !no_coq_action_required then begin
         let start, stop = get_start (), get_stop () in
-	List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
-		  Tags.Script.ephemere;
+        List.iter (fun tag -> buffer#remove_tag tag ~start ~stop)
+                  Tags.Script.ephemere;
         Sentence.tag_on_insert buffer
       end;
     end in
@@ -301,7 +301,7 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
         script#buffer#place_cursor ~where;
         script#misc#grab_focus ();
         ignore (script#scroll_to_iter
-		  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
+                  ~use_align:false ~yalign:0.75 ~within_margin:0.25 where)) in
   let tip = GMisc.label ~text:"Double click to jump to error line" () in
   let box = GPack.vbox ~homogeneous:false () in
   let () = box#pack ~expand:true table#coerce in
@@ -313,10 +313,10 @@ let create_errpage (script : Wg_ScriptView.script_view) : errpage =
     method update errs =
       if !last_update = errs then ()
       else begin
-	last_update := errs;
-	access (fun _ store -> store#clear ());
+        last_update := errs;
+        access (fun _ store -> store#clear ());
         !callback errs;
-	List.iter (fun (lno, msg) -> access (fun columns store ->
+        List.iter (fun (lno, msg) -> access (fun columns store ->
           let line = store#append () in
           store#set ~row:line ~column:(find_int_col "Line" columns) lno;
           store#set ~row:line ~column:(find_string_col "Error message" columns) msg))
@@ -333,8 +333,8 @@ let create_jobpage coqtop coqops : jobpage =
       (fun columns store tp vc ->
         let row = store#get_iter tp in
         let w = store#get ~row ~column:(find_string_col "Worker" columns) in
-	let info () = Minilib.log ("Coq busy, discarding query") in
-	Coq.try_grab coqtop (coqops#stop_worker w) info
+        let info () = Minilib.log ("Coq busy, discarding query") in
+        Coq.try_grab coqtop (coqops#stop_worker w) info
       ) in
   let tip = GMisc.label ~text:"Double click to interrupt worker" () in
   let box = GPack.vbox ~homogeneous:false () in
@@ -347,10 +347,10 @@ let create_jobpage coqtop coqops : jobpage =
     method update jobs =
       if !last_update = jobs then ()
       else begin
-	last_update := jobs;
-	access (fun _ store -> store#clear ());
+        last_update := jobs;
+        access (fun _ store -> store#clear ());
         !callback jobs;
-	CString.Map.iter (fun id job -> access (fun columns store ->
+        CString.Map.iter (fun id job -> access (fun columns store ->
           let column = find_string_col "Worker" columns in
           if job = "Dead" then
             store#foreach (fun _ row ->
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index f1a2fa4f2a..dcae3e38a5 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -93,9 +93,9 @@ object(self)
       combo, entry, ok_b in
     let r_bin =
       GBin.scrolled_window
-	~vpolicy:`AUTOMATIC
-	~hpolicy:`AUTOMATIC
-	~packing:(vbox#pack ~fill:true ~expand:true) () in
+        ~vpolicy:`AUTOMATIC
+        ~hpolicy:`AUTOMATIC
+        ~packing:(vbox#pack ~fill:true ~expand:true) () in
     let result = Wg_MessageView.message_view () in
     router#register_route route_id result;
     r_bin#add_with_viewport (result :> GObj.widget);
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index db99bc0439..c0ece1ecdc 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -11,9 +11,9 @@
 let b2c = Ideutils.byte_offset_to_char_offset
 
 class finder name (view : GText.view) =
-  
+
   let widget = Wg_Detachable.detachable
-    ~title:(Printf.sprintf "Find & Replace (%s)" name) () in 
+    ~title:(Printf.sprintf "Find & Replace (%s)" name) () in
   let replace_box = GPack.grid (* ~columns:4 ~rows:2 *) ~col_homogeneous:false ~row_homogeneous:false
     ~packing:widget#add () in
   let hb = GPack.hbox ~packing:(replace_box#attach
@@ -75,7 +75,7 @@ class finder name (view : GText.view) =
       if use_regex#active then
         if use_nocase#active then Str.regexp_case_fold rex
         else Str.regexp rex
-      else 
+      else
         if use_nocase#active then Str.regexp_string_case_fold rex
         else Str.regexp_string rex
 
@@ -94,7 +94,7 @@ class finder name (view : GText.view) =
         Some(view#buffer#start_iter#forward_chars (b2c text i),
              view#buffer#start_iter#forward_chars (b2c text j))
       with Not_found -> None
-    
+
     method private forward_search starti =
       let text = starti#get_text ~stop:view#buffer#end_iter in
       let regexp = self#regex in
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 181418d3d8..769ce61ee1 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -494,10 +494,10 @@ object (self)
       let proceed =
         if not b && i = 1 then
           iter#editable ~default:true &&
-	  iter#forward_line#editable ~default:true
+          iter#forward_line#editable ~default:true
         else if not b && i = -1 then
           iter#editable ~default:true &&
-	  iter#backward_line#editable ~default:true
+          iter#backward_line#editable ~default:true
         else false
       in
       if not proceed then GtkSignal.stop_emit ()
@@ -539,13 +539,13 @@ let script_view ct ?(source_buffer:GSourceView3.source_buffer option)  ?draw_spa
   GtkSourceView3.SourceView.make_params [] ~cont:(
     GtkText.View.make_params ~cont:(
       GContainer.pack_container ~create:
-	(fun pl ->
-	  let w = match source_buffer with
+        (fun pl ->
+          let w = match source_buffer with
             | None -> GtkSourceView3.SourceView.new_ ()
             | Some buf -> GtkSourceView3.SourceView.new_with_buffer
               (Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
-	  in
-	  let w = Gobject.unsafe_cast w in
-	  Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
+          in
+          let w = Gobject.unsafe_cast w in
+          Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
           Gaux.may ~f:(GtkSourceView3.SourceView.set_draw_spaces w) draw_spaces;
-	  ((new script_view w ct) : script_view))))
+          ((new script_view w ct) : script_view))))