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

1 files changed, 46 insertions, 46 deletions

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
-      
+