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

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 14e2e40846..28d8d5a020 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -49,9 +49,9 @@ struct
 
   type 'a t =
       {
-	outch : out_channel ;
-	mutable status : mode ;
-	htbl : 'a Table.t
+        outch : out_channel ;
+        mutable status : mode ;
+        htbl : 'a Table.t
       }
 
 
@@ -72,49 +72,49 @@ let read_key_elem inch =
     | End_of_file -> None
     | e when CErrors.noncritical e -> raise InvalidTableFormat
 
-(** 
+(**
     We used to only lock/unlock regions.
-    Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]?  
+    Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]?
     In case of locking failure, the cache is not used.
 **)
 
 type lock_kind = Read | Write
 
-let lock kd fd = 
- let pos = lseek fd 0 SEEK_CUR in 
- let success   = 
-  try 
+let lock kd fd =
+ let pos = lseek fd 0 SEEK_CUR in
+ let success   =
+  try
    ignore (lseek fd 0 SEEK_SET);
-   let lk =  match kd with 
-    | Read  -> F_RLOCK 
-    | Write -> F_LOCK in  
+   let lk =  match kd with
+    | Read  -> F_RLOCK
+    | Write -> F_LOCK in
    lockf fd lk 1; true
   with Unix.Unix_error(_,_,_) -> false in
- ignore (lseek fd pos SEEK_SET) ; 
+ ignore (lseek fd pos SEEK_SET) ;
  success
 
-let unlock fd = 
+let unlock fd =
   let pos = lseek fd 0 SEEK_CUR in
-  try 
-   ignore (lseek fd 0 SEEK_SET) ; 
+  try
+   ignore (lseek fd 0 SEEK_SET) ;
    lockf fd F_ULOCK 1
-  with 
-   Unix.Unix_error(_,_,_) -> ()    
-    (* Here, this is really bad news -- 
+  with
+   Unix.Unix_error(_,_,_) -> ()
+    (* Here, this is really bad news --
        there is a pending lock which could cause a deadlock.
        Should it be an anomaly or produce a warning ?
     *);
-  ignore (lseek fd pos SEEK_SET) 
+  ignore (lseek fd pos SEEK_SET)
 
 
 (* We make the assumption that an acquired lock can always be released *)
 
-let do_under_lock kd fd f = 
+let do_under_lock kd fd f =
  if lock kd fd
  then
   finally f (fun () -> unlock fd)
  else f ()
-  
+
 
 
 let open_in f =
@@ -128,11 +128,11 @@ let open_in f =
       | None -> ()
       | Some (key,elem) ->
           Table.add htbl key elem ;
-	  xload () in
+          xload () in
     try
       (* Locking of the (whole) file while reading *)
-      do_under_lock Read finch xload ; 
-      close_in_noerr inch ; 
+      do_under_lock Read finch xload ;
+      close_in_noerr inch ;
       {
        outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ;
        status = Open ;
@@ -145,11 +145,11 @@ let open_in f =
       let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
       let out =  (openfile f flags 0o666) in
       let outch = out_channel_of_descr out in
-      do_under_lock Write out 
-       (fun () -> 
-	Table.iter 
-	  (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
-        flush outch) ; 
+      do_under_lock Write out
+       (fun () ->
+        Table.iter
+          (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
+        flush outch) ;
       { outch = outch ;
         status = Open ;
         htbl   = htbl
@@ -165,8 +165,8 @@ let add t k e =
       let fd = descr_of_out_channel outch in
       begin
        Table.add tbl k e ;
-       do_under_lock Write fd 
-        (fun _ -> 
+       do_under_lock Write fd
+        (fun _ ->
          Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
          flush outch
         )
@@ -178,7 +178,7 @@ let find t k =
     then raise UnboundTable
     else
       let res = Table.find tbl k in
-	res
+        res
 
 let memo cache f =
   let tbl = lazy (try Some (open_in cache) with _ -> None) in
@@ -186,13 +186,13 @@ let memo cache f =
   match Lazy.force tbl with
   | None -> f x
   | Some tbl ->
-	try
-	  find tbl x
-	with
-	    Not_found ->
-	      let res = f x in
-		add tbl x res ;
-		res
+        try
+          find tbl x
+        with
+            Not_found ->
+              let res = f x in
+                add tbl x res ;
+                res
 
 let memo_cond cache cond f =
   let tbl = lazy (try Some (open_in cache) with _ -> None) in