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

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 35b64ccb8f..6fa831fda9 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -38,58 +38,58 @@ let unif evd t1 t2=
   let rec head_reduce t=
     (* forbids non-sigma-normal meta in head position*)
     match EConstr.kind evd t with
-	Meta i->
-	  (try
-	     head_reduce (Int.List.assoc i !sigma)
-	   with Not_found->t)
+        Meta i->
+          (try
+             head_reduce (Int.List.assoc i !sigma)
+           with Not_found->t)
       | _->t in
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
       let nt1=head_reduce (whd_betaiotazeta evd t1)
       and nt2=head_reduce (whd_betaiotazeta evd t2) in
-	match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
-	    Meta i,Meta j->
-	      if not (Int.equal i j) then
-		if i<j then bind j nt1
-		else bind i nt2
-	  | Meta i,_ ->
-	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels evd t) &&
+        match (EConstr.kind evd nt1),(EConstr.kind evd nt2) with
+            Meta i,Meta j->
+              if not (Int.equal i j) then
+                if i<j then bind j nt1
+                else bind i nt2
+          | Meta i,_ ->
+              let t=subst_meta !sigma nt2 in
+                if Int.Set.is_empty (free_rels evd t) &&
                   not (occur_metavariable evd i t) then
-		    bind i t else raise (UFAIL(nt1,nt2))
-	  | _,Meta i ->
-	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels evd t) &&
+                    bind i t else raise (UFAIL(nt1,nt2))
+          | _,Meta i ->
+              let t=subst_meta !sigma nt1 in
+                if Int.Set.is_empty (free_rels evd t) &&
                   not (occur_metavariable evd i t) then
-		    bind i t else raise (UFAIL(nt1,nt2))
-	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
- 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
+                    bind i t else raise (UFAIL(nt1,nt2))
+          | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
+          | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
           | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
-	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
-	      Queue.add (pa,pb) bige;
-	      Queue.add (ca,cb) bige;
-	      let l=Array.length va in
+              Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
+          | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
+              Queue.add (pa,pb) bige;
+              Queue.add (ca,cb) bige;
+              let l=Array.length va in
                 if not (Int.equal l (Array.length vb)) then
-		  raise (UFAIL (nt1,nt2))
-		else
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done
-	  | App(ha,va),App(hb,vb)->
-	      Queue.add (ha,hb) bige;
-	      let l=Array.length va in
-		if not (Int.equal l (Array.length vb)) then
-		  raise (UFAIL (nt1,nt2))
-		else
-		  for i=0 to l-1 do
-		    Queue.add (va.(i),vb.(i)) bige
-		  done
-	  | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2))
+                  raise (UFAIL (nt1,nt2))
+                else
+                  for i=0 to l-1 do
+                    Queue.add (va.(i),vb.(i)) bige
+                  done
+          | App(ha,va),App(hb,vb)->
+              Queue.add (ha,hb) bige;
+              let l=Array.length va in
+                if not (Int.equal l (Array.length vb)) then
+                  raise (UFAIL (nt1,nt2))
+                else
+                  for i=0 to l-1 do
+                    Queue.add (va.(i),vb.(i)) bige
+                  done
+          | _->if not (eq_constr_nounivs evd nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
       assert false
-	(* this place is unreachable but needed for the sake of typing *)
+        (* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
 let value evd i t=
@@ -99,7 +99,7 @@ let value evd i t=
     if isMeta evd term && Int.equal (destMeta evd term) i then 0 else
       let f v t=add v (vaux t) in
       let vr=EConstr.fold evd f (-1) term in
-	if vr<0 then -1 else vr+1 in
+        if vr<0 then -1 else vr+1 in
     vaux t
 
 type instance=
@@ -111,14 +111,14 @@ let mk_rel_inst evd t=
   let rel_env=ref [] in
   let rec renum_rec d t=
     match EConstr.kind evd t with
-	Meta n->
-	  (try
-	     mkRel (d+(Int.List.assoc n !rel_env))
-	   with Not_found->
-	     let m= !new_rel in
-	       incr new_rel;
-	       rel_env:=(n,m) :: !rel_env;
-	       mkRel (m+d))
+        Meta n->
+          (try
+             mkRel (d+(Int.List.assoc n !rel_env))
+           with Not_found->
+             let m= !new_rel in
+               incr new_rel;
+               rel_env:=(n,m) :: !rel_env;
+               mkRel (m+d))
       | _ -> EConstr.map_with_binders evd succ renum_rec d t
   in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
@@ -142,5 +142,5 @@ let more_general evd (m1,t1) (m2,t2)=
     try
       let sigma=unif evd mt1 mt2 in
       let p (n,t)= n<m1 || isMeta evd t in
-	List.for_all p sigma
+        List.for_all p sigma
     with UFAIL(_,_)->false