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

diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index f47a14cdc7..f82a55fe71 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -43,25 +43,25 @@ let rec ptrans p1 p3=
     | Trans(p1,p2), _ ->ptrans p1 (ptrans p2 p3)
     | Congr(p1,p2), Congr(p3,p4) ->pcongr (ptrans p1 p3) (ptrans p2 p4)
     | Congr(p1,p2), Trans({p_rule=Congr(p3,p4)},p5) ->
-	ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
+        ptrans (pcongr (ptrans p1 p3) (ptrans p2 p4)) p5
   | _, _ ->
       if term_equal p1.p_rhs p3.p_lhs then
-	{p_lhs=p1.p_lhs;
-	 p_rhs=p3.p_rhs;
-	 p_rule=Trans (p1,p3)}
+        {p_lhs=p1.p_lhs;
+         p_rhs=p3.p_rhs;
+         p_rule=Trans (p1,p3)}
       else anomaly (Pp.str "invalid cc transitivity.")
 
 let rec psym p =
   match p.p_rule with
       Refl _ -> p
     | SymAx s ->
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=Ax s}
+        {p_lhs=p.p_rhs;
+         p_rhs=p.p_lhs;
+         p_rule=Ax s}
     | Ax s->
-	{p_lhs=p.p_rhs;
-	 p_rhs=p.p_lhs;
-	 p_rule=SymAx s}
+        {p_lhs=p.p_rhs;
+         p_rhs=p.p_lhs;
+         p_rule=SymAx s}
   | Inject (p0,c,n,a)->
       {p_lhs=p.p_rhs;
        p_rhs=p.p_lhs;
@@ -84,9 +84,9 @@ let psymax axioms s =
 let rec nth_arg t n=
   match t with
       Appli (t1,t2)->
-	if n>0 then
-	  nth_arg t1 (n-1)
-	else t2
+        if n>0 then
+          nth_arg t1 (n-1)
+        else t2
     | _ -> anomaly ~label:"nth_arg" (Pp.str "not enough args.")
 
 let pinject p c n a =
@@ -99,7 +99,7 @@ let rec equal_proof env sigma uf i j=
   if i=j then prefl (term uf i) else
     let (li,lj)=join_path uf i j in
     ptrans (path_proof env sigma uf i li) (psym (path_proof env sigma uf j lj))
-      
+
 and edge_proof env sigma uf ((i,j),eq)=
   debug (fun () -> str "edge_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let pi=equal_proof env sigma uf i eq.lhs in
@@ -107,15 +107,15 @@ and edge_proof env sigma uf ((i,j),eq)=
   let pij=
     match eq.rule with
       Axiom (s,reversed)->
-	if reversed then psymax (axioms uf) s
-	else pax (axioms uf) s
+        if reversed then psymax (axioms uf) s
+        else pax (axioms uf) s
     | Congruence ->congr_proof env sigma uf eq.lhs eq.rhs
-    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *) 
+    | Injection (ti,ipac,tj,jpac,k) -> (* pi_k ipac = p_k jpac *)
       let p=ind_proof env sigma uf ti ipac tj jpac in
       let cinfo= get_constructor_info uf ipac.cnode in
-      pinject p cinfo.ci_constr cinfo.ci_nhyps k in  
+      pinject p cinfo.ci_constr cinfo.ci_nhyps k in
   ptrans (ptrans pi pij) pj
-  
+
 and constr_proof env sigma uf i ipac=
   debug (fun () -> str "constr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20));
   let t=find_oldest_pac uf i ipac in
@@ -128,20 +128,20 @@ and constr_proof env sigma uf i ipac=
     let targ=term uf arg in
     let p=constr_proof env sigma uf fi fipac in
     ptrans eq_it (pcongr p (prefl targ))
-      
+
 and path_proof env sigma uf i l=
   debug (fun () -> str "path_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ str "{" ++
-	   (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
+           (prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
   match l with
   | [] -> prefl (term uf i)
   | x::q->ptrans (path_proof env sigma uf (snd (fst x)) q) (edge_proof env sigma uf x)
-    
+
 and congr_proof env sigma uf i j=
   debug (fun () -> str "congr_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let (i1,i2) = subterms uf i
   and (j1,j2) = subterms uf j in
   pcongr (equal_proof env sigma uf i1 j1) (equal_proof env sigma uf i2 j2)
-    
+
 and ind_proof env sigma uf i ipac j jpac=
    debug (fun () -> str "ind_proof " ++ pr_idx_term env sigma uf i ++ brk (1,20) ++ pr_idx_term env sigma uf j);
   let p=equal_proof env sigma uf i j