[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, 24 insertions, 24 deletions

diff --git a/tactics/dn.ml b/tactics/dn.ml
index aed2c28323..e1c9b7c0b5 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -11,14 +11,14 @@ struct
     type t = (Y.t * int) option
     let compare x y =
       match x,y with
-	  None,None -> 0
-	| Some (l,n),Some (l',n') ->
-	    let m = Y.compare l l' in
-	    if Int.equal m 0 then
-	      n-n'
-	    else m
-	| Some(l,n),None -> 1
-	| None, Some(l,n) -> -1
+          None,None -> 0
+        | Some (l,n),Some (l',n') ->
+            let m = Y.compare l l' in
+            if Int.equal m 0 then
+              n-n'
+            else m
+        | Some(l,n),None -> 1
+        | None, Some(l,n) -> -1
   end
   module ZSet = Set.Make(Z)
   module X_tries =
@@ -50,12 +50,12 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
 
     and pathrec deferred t =
       match dna t with
-	| None ->
-	    None :: (path_of_deferred deferred)
-	| Some (lbl,[]) ->
-	    (Some (lbl,0))::(path_of_deferred deferred)
-	| Some (lbl,(h::def_subl as v)) ->
-	    (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
+        | None ->
+            None :: (path_of_deferred deferred)
+        | Some (lbl,[]) ->
+            (Some (lbl,0))::(path_of_deferred deferred)
+        | Some (lbl,(h::def_subl as v)) ->
+            (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h)
     in
       pathrec []
 
@@ -76,16 +76,16 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
   let lookup tm dna t =
     let rec lookrec t tm =
       match dna t with
-	| Nothing -> tm_of tm None
-	| Label(lbl,v) ->
-	    tm_of tm None@
-	      (List.fold_left
-		 (fun l c ->
-		List.flatten(List.map (fun (tm, b) ->
-					 if b then lookrec c tm
-					 else [tm,b]) l))
-		 (tm_of tm (Some(lbl,List.length v))) v)
-	| Everything -> skip_arg 1 tm
+        | Nothing -> tm_of tm None
+        | Label(lbl,v) ->
+            tm_of tm None@
+              (List.fold_left
+                 (fun l c ->
+                List.flatten(List.map (fun (tm, b) ->
+                                         if b then lookrec c tm
+                                         else [tm,b]) l))
+                 (tm_of tm (Some(lbl,List.length v))) v)
+        | Everything -> skip_arg 1 tm
     in
     List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))