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

11 files changed, 77 insertions, 77 deletions

diff --git a/clib/bigint.ml b/clib/bigint.ml
index f8625c599e..ccbc8e6322 100644
--- a/clib/bigint.ml
+++ b/clib/bigint.ml
@@ -283,15 +283,15 @@ let euclid m d =
           else
             m.(!i) / d.(0) in
         q.(!i) <- q.(!i) + v;
-	sub_mult m d v !i
+        sub_mult m d v !i
       end else begin
         let v = (m.(!i) * base + m.(!i+1)) / (d.(0) + 1) in
         q.(!i) <- q.(!i) + v / base;
-	sub_mult m d (v / base) !i;
+        sub_mult m d (v / base) !i;
         q.(!i+1) <- q.(!i+1) + v mod base;
-	if q.(!i+1) >= base then
-	  (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1);
-	sub_mult m d (v mod base) (!i+1)
+        if q.(!i+1) >= base then
+          (q.(!i+1) <- q.(!i+1)-base; q.(!i) <- q.(!i)+1);
+        sub_mult m d (v mod base) (!i+1)
       end
     done;
     (normalize q, normalize m) in
@@ -465,9 +465,9 @@ let pow  =
       let quo = m lsr 1 (* i.e. m/2 *)
       and odd = not (Int.equal (m land 1) 0) in
       pow_aux
-	(if odd then mult n odd_rest else odd_rest)
-	(mult n n)
-	quo
+        (if odd then mult n odd_rest else odd_rest)
+        (mult n n)
+        quo
   in
   pow_aux one
 
diff --git a/clib/cArray.ml b/clib/cArray.ml
index bff796ac33..be59ae57d0 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -123,7 +123,7 @@ let equal_norefl cmp t1 t2 =
 
 let equal cmp t1 t2 =
   if t1 == t2 then true else equal_norefl cmp t1 t2
-    
+
 
 let is_empty array = Int.equal (Array.length array) 0
 
diff --git a/clib/cArray.mli b/clib/cArray.mli
index 090d2bf627..f94af26515 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -110,7 +110,7 @@ sig
   (** Same with two arrays, folding on the left *)
 
   val distinct : 'a array -> bool
-  (** Return [true] if every element of the array is unique (for default 
+  (** Return [true] if every element of the array is unique (for default
       equality). *)
 
   val rev_of_list : 'a list -> 'a array
diff --git a/clib/cList.mli b/clib/cList.mli
index 9125c3b68b..d294088dc9 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -45,7 +45,7 @@ sig
   (** {6 Creating lists} *)
 
   val interval : int -> int -> int list
-  (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when 
+  (** [interval i j] creates the list [[i; i + 1; ...; j]], or [[]] when
       [j <= i]. *)
 
   val make : int -> 'a -> 'a list
diff --git a/clib/cThread.ml b/clib/cThread.ml
index 434b234ba1..953b51ed02 100644
--- a/clib/cThread.ml
+++ b/clib/cThread.ml
@@ -16,7 +16,7 @@ let thread_friendly_read_fd fd s ~off ~len =
   let rec loop () =
     try Unix.read fd s off len
     with Unix.Unix_error(Unix.EINTR,_,_) -> loop ()
-  in 
+  in
     loop ()
 
 let thread_friendly_read ic s ~off ~len =
diff --git a/clib/heap.ml b/clib/heap.ml
index daade01cb7..361f7945a4 100644
--- a/clib/heap.ml
+++ b/clib/heap.ml
@@ -129,8 +129,8 @@ module Functional(X : Ordered) = struct
 
   let rec fold f h x0 = match h with
     | Leaf ->
-	x0
+        x0
     | Node (l, x, r) ->
-	fold f l (fold f r (f x x0))
+        fold f l (fold f r (f x x0))
 
 end
diff --git a/clib/option.ml b/clib/option.ml
index fd88257238..17024e988b 100644
--- a/clib/option.ml
+++ b/clib/option.ml
@@ -200,8 +200,8 @@ module List =
   let rec find f = function
     | [] -> None
     | h :: t -> match f h with
-	 | None -> find f t
-	 | x -> x
+         | None -> find f t
+         | x -> x
 
   let map f l =
     let rec aux f l = match l with
diff --git a/clib/predicate.mli b/clib/predicate.mli
index cee3b0bd39..d599b92dd4 100644
--- a/clib/predicate.mli
+++ b/clib/predicate.mli
@@ -9,7 +9,7 @@ module type OrderedType =
     type t
     (** The type of the elements in the set.
 
-	The chosen [t] {b must be infinite}. *)
+        The chosen [t] {b must be infinite}. *)
 
     val compare : t -> t -> int
     (** A total ordering function over the set elements.
diff --git a/clib/segmenttree.ml b/clib/segmenttree.ml
index 3518fc130d..b22a9b921c 100644
--- a/clib/segmenttree.ml
+++ b/clib/segmenttree.ml
@@ -11,7 +11,7 @@
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of
-    disjoint segments to some values of type 'a. 
+    disjoint segments to some values of type 'a.
 *)
 
 (** Misc. functions. *)
@@ -24,15 +24,15 @@ let list_iteri f l =
 
 let log2 x = log x /. log 2.
 
-let log2n x = int_of_float (ceil (log2 (float_of_int x))) 
+let log2n x = int_of_float (ceil (log2 (float_of_int x)))
 
 (** We focus on integers but this module can be generalized. *)
 type elt = int
 
-(** A value of type [domain] is interpreted differently given its position 
-    in the tree. On internal nodes, a domain represents the set of 
-    integers which are _not_ in the set of keys handled by the tree. On 
-    leaves, a domain represents the st of integers which are in the set of 
+(** A value of type [domain] is interpreted differently given its position
+    in the tree. On internal nodes, a domain represents the set of
+    integers which are _not_ in the set of keys handled by the tree. On
+    leaves, a domain represents the st of integers which are in the set of
     keys. *)
 type domain =
   | Interval of elt * elt
@@ -61,14 +61,14 @@ let right_child i = 2 * i + 2
 let value_of i t = match t.(i) with (_, Some x) -> x | _ -> raise Not_found
 
 (** Initialize the array to store [n] leaves. *)
-let create n init = 
+let create n init =
   Array.make (1 lsl (log2n n + 1) - 1) init
 
-(** Make a complete interval tree from a list of disjoint segments. 
+(** Make a complete interval tree from a list of disjoint segments.
     Precondition : the segments must be sorted. *)
-let make segments = 
+let make segments =
   let nsegments = List.length segments in
-  let tree = create nsegments (Universe, None) in 
+  let tree = create nsegments (Universe, None) in
   let leaves_offset = (1 lsl (log2n nsegments)) - 1 in
 
     (* The algorithm proceeds in two steps using an intermediate tree
@@ -79,62 +79,62 @@ let make segments =
        with the given segments... *)
     list_iteri
       (fun i ((start, stop), value) ->
-	 let k = leaves_offset + i in
-	 let i = Interval (start, stop) in
-	   tree.(k) <- (i, Some i))
+         let k = leaves_offset + i in
+         let i = Interval (start, stop) in
+           tree.(k) <- (i, Some i))
       segments;
     (* ... the remaining leaves are initialized with neutral information. *)
-    for k = leaves_offset + nsegments to Array.length tree -1 do 
+    for k = leaves_offset + nsegments to Array.length tree -1 do
       tree.(k) <- (Universe, Some Universe)
     done;
-    
+
     (* We traverse the tree bottom-up and compute the interval and
        annotation associated to each node from the annotations of its
        children. *)
     for k = leaves_offset - 1 downto 0 do
-      let node, annotation = 
-	match value_of (left_child k) tree, value_of (right_child k) tree with
-	  | Interval (left_min, left_max), Interval (right_min, right_max) ->
-	      (Interval (left_max, right_min), Interval (left_min, right_max))
-	  | Interval (min, max), Universe -> 
-	      (Interval (max, max), Interval (min, max))
-	  | Universe, Universe -> Universe, Universe
-	  | Universe, _ -> assert false
+      let node, annotation =
+        match value_of (left_child k) tree, value_of (right_child k) tree with
+          | Interval (left_min, left_max), Interval (right_min, right_max) ->
+              (Interval (left_max, right_min), Interval (left_min, right_max))
+          | Interval (min, max), Universe ->
+              (Interval (max, max), Interval (min, max))
+          | Universe, Universe -> Universe, Universe
+          | Universe, _ -> assert false
       in
-	tree.(k) <- (node, Some annotation)
+        tree.(k) <- (node, Some annotation)
     done;
 
     (* Finally, annotation are replaced with the image related to each leaf. *)
-    let final_tree = 
+    let final_tree =
       Array.mapi (fun i (segment, value) -> (segment, None)) tree
     in
-      list_iteri 
-	(fun i ((start, stop), value) -> 
-	   final_tree.(leaves_offset + i) 
-	   <- (Interval (start, stop), Some value))
-	segments;      
+      list_iteri
+        (fun i ((start, stop), value) ->
+           final_tree.(leaves_offset + i)
+           <- (Interval (start, stop), Some value))
+        segments;
       final_tree
 
-(** [lookup k t] looks for an image for key [k] in the interval tree [t]. 
+(** [lookup k t] looks for an image for key [k] in the interval tree [t].
     Raise [Not_found] if it fails. *)
-let lookup k t = 
-  let i = ref 0 in 
+let lookup k t =
+  let i = ref 0 in
     while (snd t.(!i) = None) do
       match fst t.(!i) with
-	| Interval (start, stop) -> 
-	    if k <= start then i := left_child !i
-	    else if k >= stop then i:= right_child !i 
-	    else raise Not_found
-	| Universe -> raise Not_found
+        | Interval (start, stop) ->
+            if k <= start then i := left_child !i
+            else if k >= stop then i:= right_child !i
+            else raise Not_found
+        | Universe -> raise Not_found
     done;
     match fst t.(!i) with
-      | Interval (start, stop) -> 
-	  if k >= start && k <= stop then
-	    match snd t.(!i) with 
-	      | Some v -> v
-	      | None -> assert false
-	  else 
-	    raise Not_found
+      | Interval (start, stop) ->
+          if k >= start && k <= stop then
+            match snd t.(!i) with
+              | Some v -> v
+              | None -> assert false
+          else
+            raise Not_found
       | Universe -> assert false
-      
+
 
diff --git a/clib/segmenttree.mli b/clib/segmenttree.mli
index fa198f7ad6..eb2a7569fd 100644
--- a/clib/segmenttree.mli
+++ b/clib/segmenttree.mli
@@ -11,7 +11,7 @@
 (** This module is a very simple implementation of "segment trees".
 
     A segment tree of type ['a t] represents a mapping from a union of
-    disjoint segments to some values of type 'a. 
+    disjoint segments to some values of type 'a.
 *)
 
 (** A mapping from a union of disjoint segments to some values of type ['a]. *)
@@ -19,11 +19,11 @@ type 'a t
 
 (** [make [(i1, j1), v1; (i2, j2), v2; ...]] creates a mapping that
     associates to every integer [x] the value [v1] if [i1 <= x <= j1],
-    [v2] if [i2 <= x <= j2], and so one. 
+    [v2] if [i2 <= x <= j2], and so one.
     Precondition: the segments must be sorted. *)
 val make : ((int * int) * 'a) list -> 'a t
 
-(** [lookup k t] looks for an image for key [k] in the interval tree [t]. 
+(** [lookup k t] looks for an image for key [k] in the interval tree [t].
     Raise [Not_found] if it fails. *)
 val lookup : int -> 'a t -> 'a
 
diff --git a/clib/unionfind.ml b/clib/unionfind.ml
index 4de9fb8faa..8b7918a020 100644
--- a/clib/unionfind.ml
+++ b/clib/unionfind.ml
@@ -99,9 +99,9 @@ module Make (S:SetS)(M:MapS with type key = S.elt) = struct
     match !node with
       | Canon _ -> x, node
       | Equiv y ->
-	let ((z,_) as res) = lookup y p in
-	if not (z == y) then node := Equiv z;
-	res
+        let ((z,_) as res) = lookup y p in
+        if not (z == y) then node := Equiv z;
+        res
 
   let add x p = if not (M.mem x !p) then ignore (fresh x p)
 
@@ -117,10 +117,10 @@ module Make (S:SetS)(M:MapS with type key = S.elt) = struct
       let xcan, ycan = if x < y then xcan, ycan else ycan, xcan in
       let x,xnode = xcan and y,ynode = ycan in
       match !xnode, !ynode with
-	| Canon lx, Canon ly ->
-	  xnode := Canon (S.union lx ly);
-	  ynode := Equiv x;
-	| _ -> assert false
+        | Canon lx, Canon ly ->
+          xnode := Canon (S.union lx ly);
+          ynode := Equiv x;
+        | _ -> assert false
 
   let union_set s p =
     try
@@ -130,9 +130,9 @@ module Make (S:SetS)(M:MapS with type key = S.elt) = struct
 
   let partition p =
     List.rev (M.fold
-		(fun x node acc -> match !node with
-		  | Equiv _ -> acc
-		  | Canon lx -> lx::acc)
-		!p [])
+                (fun x node acc -> match !node with
+                  | Equiv _ -> acc
+                  | Canon lx -> lx::acc)
+                !p [])
 
 end