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

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index e53412383c..9ff05c33e4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -23,37 +23,37 @@ let newcnt ()=
 let priority = (* pure heuristics, <=0 for non reversible *)
   function
       Right rf->
-	begin
-	  match rf with
-	      Rarrow               -> 100
-	    | Rand                 ->  40
-	    | Ror                  -> -15
-	    | Rfalse               -> -50
-	    | Rforall              -> 100
-	    | Rexists (_,_,_)      -> -29
-	end
+        begin
+          match rf with
+              Rarrow               -> 100
+            | Rand                 ->  40
+            | Ror                  -> -15
+            | Rfalse               -> -50
+            | Rforall              -> 100
+            | Rexists (_,_,_)      -> -29
+        end
     | Left lf ->
-	match lf with
-	    Lfalse                 -> 999
-	  | Land _                 ->  90
-	  | Lor _                  ->  40
-	  | Lforall (_,_,_)        -> -30
-	  | Lexists _              ->  60
-	  | LA(_,lap) ->
-	      match lap with
-		  LLatom           ->   0
-		| LLfalse (_,_)    -> 100
-		| LLand (_,_)      ->  80
-		| LLor (_,_)       ->  70
-		| LLforall _       -> -20
-		| LLexists (_,_)   ->  50
-		| LLarrow  (_,_,_) -> -10
+        match lf with
+            Lfalse                 -> 999
+          | Land _                 ->  90
+          | Lor _                  ->  40
+          | Lforall (_,_,_)        -> -30
+          | Lexists _              ->  60
+          | LA(_,lap) ->
+              match lap with
+                  LLatom           ->   0
+                | LLfalse (_,_)    -> 100
+                | LLand (_,_)      ->  80
+                | LLor (_,_)       ->  70
+                | LLforall _       -> -20
+                | LLexists (_,_)   ->  50
+                | LLarrow  (_,_,_) -> -10
 
 module OrderedFormula=
 struct
   type t=Formula.t
   let compare e1 e2=
-	(priority e1.pat) - (priority e2.pat)
+        (priority e1.pat) - (priority e2.pat)
 end
 
 type h_item = GlobRef.t * (int*Constr.t) option
@@ -89,8 +89,8 @@ let cm_remove sigma typ nam cm=
     let l=CM.find typ cm in
     let l0=List.filter (fun id-> not (GlobRef.equal id nam)) l in
       match l0 with
-	  []->CM.remove typ cm
-	| _ ->CM.add typ l0 cm
+          []->CM.remove typ cm
+        | _ ->CM.add typ l0 cm
       with Not_found ->cm
 
 module HP=Heap.Functional(OrderedFormula)
@@ -114,35 +114,35 @@ let lookup sigma item seq=
   match item with
       (_,None)->false
     | (id,Some (m, t))->
-	let p (id2,o)=
-	  match o with
-	      None -> false
+        let p (id2,o)=
+          match o with
+              None -> false
             | Some (m2, t2)-> GlobRef.equal id id2 && m2>m && more_general sigma (m2, EConstr.of_constr t2) (m, EConstr.of_constr t) in
-	  History.exists p seq.history
+          History.exists p seq.history
 
 let add_formula env sigma side nam t seq =
   match build_formula env sigma side nam t seq.cnt with
       Left f->
-	begin
-	  match side with
-	      Concl ->
-		{seq with
-		   redexes=HP.add f seq.redexes;
-		   gl=f.constr;
-		   glatom=None}
-	    | _ ->
-		{seq with
-		   redexes=HP.add f seq.redexes;
-		   context=cm_add sigma f.constr nam seq.context}
-	end
+        begin
+          match side with
+              Concl ->
+                {seq with
+                   redexes=HP.add f seq.redexes;
+                   gl=f.constr;
+                   glatom=None}
+            | _ ->
+                {seq with
+                   redexes=HP.add f seq.redexes;
+                   context=cm_add sigma f.constr nam seq.context}
+        end
     | Right t->
-	match side with
-	    Concl ->
-	      {seq with gl=t;glatom=Some t}
-	  | _ ->
-	      {seq with
-		 context=cm_add sigma t nam seq.context;
-		 latoms=t::seq.latoms}
+        match side with
+            Concl ->
+              {seq with gl=t;glatom=Some t}
+          | _ ->
+              {seq with
+                 context=cm_add sigma t nam seq.context;
+                 latoms=t::seq.latoms}
 
 let re_add_formula_list sigma lf seq=
   let do_one f cm=
@@ -166,14 +166,14 @@ let rec take_formula sigma seq=
   and hp=HP.remove seq.redexes in
     if hd.id == dummy_id then
       let nseq={seq with redexes=hp} in
-	if seq.gl==hd.constr then
-	  hd,nseq
-	else
-	  take_formula sigma nseq (* discarding deprecated goal *)
+        if seq.gl==hd.constr then
+          hd,nseq
+        else
+          take_formula sigma nseq (* discarding deprecated goal *)
     else
       hd,{seq with
-	    redexes=hp;
-	    context=cm_remove sigma hd.constr hd.id seq.context}
+            redexes=hp;
+            context=cm_remove sigma hd.constr hd.id seq.context}
 
 let empty_seq depth=
   {redexes=HP.empty;
@@ -191,7 +191,7 @@ let expand_constructor_hints =
         List.init (Inductiveops.nconstructors (Global.env()) ind)
           (fun i -> GlobRef.ConstructRef (ind,i+1))
     | gr ->
-	[gr])
+        [gr])
 
 let extend_with_ref_list env sigma l seq =
   let l = expand_constructor_hints l in
@@ -207,22 +207,22 @@ let extend_with_auto_hints env sigma l seq =
   let seqref=ref seq in
   let f p_a_t =
     match repr_hint p_a_t.code with
-	Res_pf (c,_) | Give_exact (c,_)
+        Res_pf (c,_) | Give_exact (c,_)
       | Res_pf_THEN_trivial_fail (c,_) ->
           let (c, _, _) = c in
-	  (try
-	     let (gr, _) = Termops.global_of_constr sigma c in
-	     let typ=(Typing.unsafe_type_of env sigma c) in
-	       seqref:=add_formula env sigma Hint gr typ !seqref
-	   with Not_found->())
+          (try
+             let (gr, _) = Termops.global_of_constr sigma c in
+             let typ=(Typing.unsafe_type_of env sigma c) in
+               seqref:=add_formula env sigma Hint gr typ !seqref
+           with Not_found->())
       | _-> () in
   let g _ _ l = List.iter f l in
   let h dbname=
     let hdb=
       try
-	searchtable_map dbname
+        searchtable_map dbname
       with Not_found->
-	user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
+        user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in
       Hint_db.iter g hdb in
     List.iter h l;
     !seqref, sigma (*FIXME: forgetting about universes*)
@@ -239,9 +239,9 @@ let print_cmap map=
       cut () ++
       s in
     (v 0
-	     (str "-----" ++
-	      cut () ++
-	      CM.fold print_entry map (mt ()) ++
-	      str "-----"))
+             (str "-----" ++
+              cut () ++
+              CM.fold print_entry map (mt ()) ++
+              str "-----"))