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

diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index ef610ce7e9..c3710cb0d6 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -23,41 +23,41 @@ let rec conv_val env pb lvl v1 v2 cu =
   else
     match kind_of_value v1, kind_of_value v2 with
     | Vfun f1, Vfun f2 ->
-	let v = mk_rel_accu lvl in
-	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+        let v = mk_rel_accu lvl in
+        conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
     | Vfun _f1, _ ->
-	conv_val env CONV lvl v1 (fun x -> v2 x) cu
+        conv_val env CONV lvl v1 (fun x -> v2 x) cu
     | _, Vfun _f2 ->
-	conv_val env CONV lvl (fun x -> v1 x) v2 cu
+        conv_val env CONV lvl (fun x -> v1 x) v2 cu
     | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl k1 k2 cu
-    | Vconst i1, Vconst i2 -> 
-	if Int.equal i1 i2 then cu else raise NotConvertible
+        conv_accu env pb lvl k1 k2 cu
+    | Vconst i1, Vconst i2 ->
+        if Int.equal i1 i2 then cu else raise NotConvertible
     | Vint64 i1, Vint64 i2 ->
       if Int64.equal i1 i2 then cu else raise NotConvertible
     | Vfloat64 f1, Vfloat64 f2 ->
         if Float64.(equal (of_float f1) (of_float f2)) then cu
         else raise NotConvertible
     | Vblock b1, Vblock b2 ->
-	let n1 = block_size b1 in
+        let n1 = block_size b1 in
         let n2 = block_size b2 in
-	if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
-	  raise NotConvertible;
-	let rec aux lvl max b1 b2 i cu =
-	  if Int.equal i max then 
-	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
-	  else
-	    let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
-	    aux lvl max b1 b2 (i+1) cu
-	in
-	aux lvl (n1-1) b1 b2 0 cu
+        if not (Int.equal (block_tag b1) (block_tag b2)) || not (Int.equal n1 n2) then
+          raise NotConvertible;
+        let rec aux lvl max b1 b2 i cu =
+          if Int.equal i max then
+            conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
+          else
+            let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+            aux lvl max b1 b2 (i+1) cu
+        in
+        aux lvl (n1-1) b1 b2 0 cu
     | (Vaccu _ | Vconst _ | Vint64 _ | Vfloat64 _ | Vblock _), _ -> raise NotConvertible
 
 and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
-  if Int.equal n1 0 then 
+  if Int.equal n1 0 then
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
     let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
@@ -73,48 +73,48 @@ and conv_atom env pb lvl a1 a2 cu =
       if Evar.equal ev1 ev2 then
         Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
       else raise NotConvertible
-    | Arel i1, Arel i2 -> 
-	if Int.equal i1 i2 then cu else raise NotConvertible
+    | Arel i1, Arel i2 ->
+        if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind (ind1,u1), Aind (ind2,u2) ->
        if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
        else raise NotConvertible
     | Aconstant (c1,u1), Aconstant (c2,u2) ->
        if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
        else raise NotConvertible
-    | Asort s1, Asort s2 -> 
+    | Asort s1, Asort s2 ->
         sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if Id.equal id1 id2 then cu else raise NotConvertible
+        if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
-	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	let cu = conv_accu env CONV lvl ac1 ac2 cu in
-	let tbl = a1.asw_reloc in
-	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
-	else begin
-	    let cu = conv_val env CONV lvl p1 p2 cu in
-	    let max = len - 1 in
-	    let rec aux i cu =
-	      let tag,arity = tbl.(i) in
-	      let ci =
-		if Int.equal arity 0 then mk_const tag
-		else mk_block tag (mk_rels_accu lvl arity) in
-	      let bi1 = bs1 ci and bi2 = bs2 ci in
-	      if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
-	      else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
-	    aux 0 cu
-	  end
+        if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
+        let cu = conv_accu env CONV lvl ac1 ac2 cu in
+        let tbl = a1.asw_reloc in
+        let len = Array.length tbl in
+        if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
+        else begin
+            let cu = conv_val env CONV lvl p1 p2 cu in
+            let max = len - 1 in
+            let rec aux i cu =
+              let tag,arity = tbl.(i) in
+              let ci =
+                if Int.equal arity 0 then mk_const tag
+                else mk_block tag (mk_rels_accu lvl arity) in
+              let bi1 = bs1 ci and bi2 = bs2 ci in
+              if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+              else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+            aux 0 cu
+          end
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
-	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
-	if f1 == f2 then cu
-	else conv_fix env lvl t1 f1 t2 f2 cu
+        if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
+        if f1 == f2 then cu
+        else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
-	if not (Int.equal s1 s2) then raise NotConvertible;
-	if f1 == f2 then cu
-	else
-	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
-	  else conv_fix env lvl t1 f1 t2 f2 cu 
+        if not (Int.equal s1 s2) then raise NotConvertible;
+        if f1 == f2 then cu
+        else
+          if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
+          else conv_fix env lvl t1 f1 t2 f2 cu
     | Aprod(_,d1,_c1), Aprod(_,d2,_c2) ->
        let cu = conv_val env CONV lvl d1 d2 cu in
        let v = mk_rel_accu lvl in