[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
```

13 files changed, 79 insertions, 79 deletions

diff --git a/lib/cProfile.ml b/lib/cProfile.ml
index 323a14c6f0..34656ef4d5 100644
--- a/lib/cProfile.ml
+++ b/lib/cProfile.ml
@@ -134,7 +134,7 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
   begin
     (try
        let c =
-	 open_out_gen
+         open_out_gen
            [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 filename in
        output_binary_int c magic;
        output_value c updated_data;
@@ -246,7 +246,7 @@ let time_overhead_A_D () =
       p.intcount <- p.intcount + e.intcount - intcount0 + 1;
       p.immcount <- p.immcount + 1;
       if not (p==e) then
-	(match !dummy_stack with [] -> assert false | _::s -> stack := s);
+        (match !dummy_stack with [] -> assert false | _::s -> stack := s);
       dummy_last_alloc := get_alloc ()
   done;
   let after = get_time () in
@@ -328,30 +328,30 @@ let close_profile print =
       let t = get_time () in
       match !stack with
       | [outside] ->
-	  outside.tottime <- outside.tottime + t;
-	  outside.owntime <- outside.owntime + t;
-	  ajoute_ownalloc outside dw;
-	  ajoute_totalloc outside dw;
-	  let ov_bc = time_overhead_B_C () (* B+C overhead *) in
-	  let ov_ad = time_overhead_A_D () (* A+D overhead *) in
-	  let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
-	  let adjtable = List.map adjust !prof_table in
-	  let adjoutside = adjust_time ov_bc ov_ad outside in
-	  let totalloc = !last_alloc -. !init_alloc in
-	  let total = create_record () in
-	  total.tottime <- outside.tottime;
-	  total.totalloc <- totalloc;
-	  (* We compute estimations of overhead, put into "own" fields *)
-	  total.owntime <- outside.tottime - adjoutside.tottime;
-	  total.ownalloc <- totalloc -. outside.totalloc;
-	  let current_data = (adjtable, adjoutside, total) in
-	  let updated_data =
-	    match !recording_file with
-	      |	"" -> current_data
-	      | name -> merge_profile !recording_file current_data
-	  in
-	  if print then format_profile updated_data;
-	  init_profile ()
+          outside.tottime <- outside.tottime + t;
+          outside.owntime <- outside.owntime + t;
+          ajoute_ownalloc outside dw;
+          ajoute_totalloc outside dw;
+          let ov_bc = time_overhead_B_C () (* B+C overhead *) in
+          let ov_ad = time_overhead_A_D () (* A+D overhead *) in
+          let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in
+          let adjtable = List.map adjust !prof_table in
+          let adjoutside = adjust_time ov_bc ov_ad outside in
+          let totalloc = !last_alloc -. !init_alloc in
+          let total = create_record () in
+          total.tottime <- outside.tottime;
+          total.totalloc <- totalloc;
+          (* We compute estimations of overhead, put into "own" fields *)
+          total.owntime <- outside.tottime - adjoutside.tottime;
+          total.ownalloc <- totalloc -. outside.totalloc;
+          let current_data = (adjtable, adjoutside, total) in
+          let updated_data =
+            match !recording_file with
+              |	"" -> current_data
+              | name -> merge_profile !recording_file current_data
+          in
+          if print then format_profile updated_data;
+          init_profile ()
       | _ -> failwith "Inconsistency"
     end
 
diff --git a/lib/cProfile.mli b/lib/cProfile.mli
index 6f8639226d..50dd6bec34 100644
--- a/lib/cProfile.mli
+++ b/lib/cProfile.mli
@@ -111,11 +111,11 @@ val profile8 :
 (** Some utilities to compute the logical and physical sizes and depth
    of ML objects *)
 
-(** Print logical size (in words) and depth of its argument 
+(** Print logical size (in words) and depth of its argument
    This function does not disturb the heap *)
 val print_logical_stats : 'a -> unit
 
-(** Print physical size, logical size (in words) and depth of its argument 
+(** Print physical size, logical size (in words) and depth of its argument
    This function allocates itself a lot (the same order of magnitude
    as the physical size of its argument) *)
 val print_stats : 'a -> unit
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index 7612e8c340..0f2c083042 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -34,7 +34,7 @@ let add_warning_in_category ~name ~category =
 
 let set_warning_status ~name status =
   try
-    let w = Hashtbl.find warnings name in 
+    let w = Hashtbl.find warnings name in
     Hashtbl.replace warnings name { w with status = status }
   with Not_found -> ()
 
diff --git a/lib/envars.ml b/lib/envars.ml
index 440df08782..67759d0a3e 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -29,8 +29,8 @@ let home ~warn =
   getenv_else "HOME" (fun () ->
     try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
       getenv_else "USERPROFILE" (fun () ->
-	warn ("Cannot determine user home directory, using '.' .");
-	Filename.current_dir_name))
+        warn ("Cannot determine user home directory, using '.' .");
+        Filename.current_dir_name))
 
 let path_to_list p =
   let sep = if String.equal Sys.os_type "Win32" then ';' else ':' in
@@ -46,20 +46,20 @@ let expand_path_macros ~warn s =
     let l = String.length s in
     if Int.equal i l then s else
       match s.[i] with
-	| '$' ->
-	  let n = expand_atom s (i+1) in
-	  let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in
-	  let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
-	  expand_macros s (i + String.length v)
-	| '~' when Int.equal i 0 ->
-	  let n = expand_atom s (i+1) in
-	  let v =
-	    if Int.equal n (i + 1) then home ~warn
-	    else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir
-	  in
-	  let s = v^(String.sub s n (l-n)) in
-	  expand_macros s (String.length v)
-	| c -> expand_macros s (i+1)
+        | '$' ->
+          let n = expand_atom s (i+1) in
+          let v = safe_getenv warn (String.sub s (i+1) (n-i-1)) in
+          let s = (String.sub s 0 i)^v^(String.sub s n (l-n)) in
+          expand_macros s (i + String.length v)
+        | '~' when Int.equal i 0 ->
+          let n = expand_atom s (i+1) in
+          let v =
+            if Int.equal n (i + 1) then home ~warn
+            else (Unix.getpwnam (String.sub s (i+1) (n-i-1))).Unix.pw_dir
+          in
+          let s = v^(String.sub s n (l-n)) in
+          expand_macros s (String.length v)
+        | c -> expand_macros s (i+1)
   in expand_macros s 0
 
 (** {1 Paths} *)
@@ -172,7 +172,7 @@ let xdg_dirs ~warn =
 (* Print the configuration information *)
 
 let print_config ?(prefix_var_name="") f coq_src_subdirs =
-  let open Printf in 
+  let open Printf in
   fprintf f "%sLOCAL=%s\n" prefix_var_name (if Coq_config.local then "1" else "0");
   fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ());
   fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ());
diff --git a/lib/envars.mli b/lib/envars.mli
index db904d419d..9f65ef8557 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -8,20 +8,20 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This file provides a high-level interface to the environment variables 
+(** This file provides a high-level interface to the environment variables
     needed by Coq to run (such as coqlib). The values of these variables
-    may come from different sources (shell environment variables, 
+    may come from different sources (shell environment variables,
     command line options, options set at the time Coq was build). *)
 
-(** [expand_path_macros warn s] substitutes environment variables 
+(** [expand_path_macros warn s] substitutes environment variables
     in a string by their values. This function also takes care of
-    substituting path of the form '~X' by an absolute path. 
+    substituting path of the form '~X' by an absolute path.
     Use [warn] as a message displayer. *)
 val expand_path_macros : warn:(string -> unit) -> string -> string
 
 (** [home warn] returns the root of the user directory, depending
-    on the OS. This information is usually stored in the $HOME 
-    environment variable on POSIX shells. If no such variable 
+    on the OS. This information is usually stored in the $HOME
+    environment variable on POSIX shells. If no such variable
     exists, then other common names are tried (HOMEDRIVE, HOMEPATH,
     USERPROFILE). If all of them fail, [warn] is called. *)
 val home : warn:(string -> unit) -> string
@@ -47,14 +47,14 @@ val set_user_coqlib : string -> unit
 (** [coqbin] is the name of the current executable. *)
 val coqbin : string
 
-(** [coqroot] is the path to [coqbin]. 
+(** [coqroot] is the path to [coqbin].
     The following value only makes sense when executables are running from
-    source tree (e.g. during build or in local mode). 
+    source tree (e.g. during build or in local mode).
 *)
 val coqroot : string
 
-(** [coqpath] is the standard path to coq. 
-    Notice that coqpath is stored in reverse order, since that is 
+(** [coqpath] is the standard path to coq.
+    Notice that coqpath is stored in reverse order, since that is
     the order it gets added to the search path. *)
 val coqpath : string list
 
diff --git a/lib/explore.ml b/lib/explore.ml
index e30dd7e809..42d48fbc1b 100644
--- a/lib/explore.ml
+++ b/lib/explore.ml
@@ -48,7 +48,7 @@ module Make = functor(S : SearchProblem) -> struct
       | [] -> raise Not_found
       | [s] -> explore (i::p) s
       | s :: l ->
-	  try explore (i::p) s with Not_found -> explore_many (succ i) p l
+          try explore (i::p) s with Not_found -> explore_many (succ i) p l
     in
     explore [1] s
 
@@ -82,11 +82,11 @@ module Make = functor(S : SearchProblem) -> struct
       enqueue 1 p q' (S.branching s)
     and enqueue i p q = function
       | [] ->
-	  explore q
+          explore q
       | s :: l ->
-	  let ps = i::p in
-	  msg_with_position ps (S.pp s);
-	  if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
+          let ps = i::p in
+          msg_with_position ps (S.pp s);
+          if S.success s then s else enqueue (succ i) p (push (ps,s) q) l
     in
     enqueue 1 [] empty [s]
 
diff --git a/lib/pp.ml b/lib/pp.ml
index 2f780677d9..3e9ab2a82b 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -265,7 +265,7 @@ let prlist_sep_lastsep no_empty sep_thunk lastsep_thunk elem l =
     | h::t   -> h ++ sep ++ insert_seps t
   in
   insert_seps filtered_elems
-  
+
 let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l
 (* [prlist_with_sep sep pr [a ; ... ; c]] outputs
    [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
diff --git a/lib/pp.mli b/lib/pp.mli
index b97e74132c..7bb66b0135 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -149,8 +149,8 @@ val prlist_strict :  ('a -> t) -> 'a list -> t
 val prlist_with_sep :
    (unit -> t) -> ('a -> t) -> 'a list -> t
 (** [prlist_with_sep sep pr [a ; ... ; c]] outputs
-    [pr a ++ sep () ++ ... ++ sep () ++ pr c]. 
-    where the thunk sep is memoized, rather than being called each place 
+    [pr a ++ sep () ++ ... ++ sep () ++ pr c].
+    where the thunk sep is memoized, rather than being called each place
      its result is used.
 *)
 
diff --git a/lib/spawn.ml b/lib/spawn.ml
index ea0cef54f6..046829802b 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -209,8 +209,8 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
   p, cout
 
 let rec wait p =
-  (* On windows kill is not reliable, so wait may never return. *) 
-  if Sys.os_type = "Unix" then 
+  (* On windows kill is not reliable, so wait may never return. *)
+  if Sys.os_type = "Unix" then
     try snd (Unix.waitpid [] p.pid)
     with
     | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
@@ -254,8 +254,8 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
   with e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let rec wait p =
-  (* On windows kill is not reliable, so wait may never return. *) 
-  if Sys.os_type = "Unix" then 
+  (* On windows kill is not reliable, so wait may never return. *)
+  if Sys.os_type = "Unix" then
     try snd (Unix.waitpid [] p.pid)
     with
     | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
diff --git a/lib/spawn.mli b/lib/spawn.mli
index 5321436ab0..03613fc4ec 100644
--- a/lib/spawn.mli
+++ b/lib/spawn.mli
@@ -27,7 +27,7 @@ module type Control = sig
   val kill : handle -> unit
   val wait : handle -> Unix.process_status
   val unixpid : handle -> int
-  
+
   (* What is used in debug messages *)
   val uid : handle -> string
 
@@ -54,7 +54,7 @@ module Async(ML : MainLoopModel) : sig
   (* If the returned value is false the callback is never called again and
    * the process is killed *)
   type callback = ML.condition list -> read_all:(unit -> string) -> bool
-  
+
   val spawn :
     ?prefer_sock:bool -> ?env:string array -> string -> string array ->
       callback -> process * out_channel
@@ -65,7 +65,7 @@ end
 (* spawn a process and read its output synchronously *)
 module Sync () : sig
   type process
-  
+
   val spawn :
     ?prefer_sock:bool -> ?env:string array -> string -> string array ->
       process * in_channel * out_channel
diff --git a/lib/system.ml b/lib/system.ml
index 8c333ec267..2d68fd2fdf 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -29,9 +29,9 @@ let all_subdirs ~unix_path:root =
   let rec traverse path rel =
     let f = function
       | FileDir (path,f) ->
-	  let newrel = rel @ [f] in
-	  add path newrel;
-	  traverse path newrel
+          let newrel = rel @ [f] in
+          add path newrel;
+          traverse path newrel
       | _ -> ()
     in process_directory f path
   in
@@ -133,7 +133,7 @@ let find_file_in_path ?(warn=true) paths filename =
       root, filename
     else
       CErrors.user_err ~hdr:"System.find_file_in_path"
-	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
+        (hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
     (* the name is considered to be the transcription as a relative
        physical name of a logical name, so we deal with it as a name
@@ -141,8 +141,8 @@ let find_file_in_path ?(warn=true) paths filename =
     try where_in_path ~warn paths filename
     with Not_found ->
       CErrors.user_err ~hdr:"System.find_file_in_path"
-	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
-		str "on loadpath"))
+        (hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
+                str "on loadpath"))
 
 let is_in_path lpath filename =
   try ignore (where_in_path ~warn:false lpath filename); true
diff --git a/lib/util.ml b/lib/util.ml
index 61678f7669..e2447b005e 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -97,7 +97,7 @@ let matrix_transpose mat =
 let identity x = x
 
 (** Left-to-right function composition:
-    
+
     [f1 %> f2] is [fun x -> f2 (f1 x)].
 
     [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].
diff --git a/lib/util.mli b/lib/util.mli
index b6347126e0..2f1a03a19c 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -94,7 +94,7 @@ val matrix_transpose : 'a list list -> 'a list list
 val identity : 'a -> 'a
 
 (** Left-to-right function composition:
-    
+
     [f1 %> f2] is [fun x -> f2 (f1 x)].
 
     [f1 %> f2 %> f3] is [fun x -> f3 (f2 (f1 x))].