[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
```

9 files changed, 437 insertions, 437 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index fb363b9393..38dd8992bc 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -41,7 +41,7 @@ let meta_succ m = m+1
 let rec nb_prod_after n c=
   match Constr.kind c with
     | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
-	1+(nb_prod_after 0 b)
+        1+(nb_prod_after 0 b)
     | _ -> 0
 
 let construct_nhyps env ind =
@@ -82,40 +82,40 @@ let kind_of_formula env sigma term =
   let normalize = special_nf env sigma in
   let cciterm = special_whd env sigma term in
     match match_with_imp_term env sigma cciterm with
-	Some (a,b)-> Arrow (a, pop b)
+        Some (a,b)-> Arrow (a, pop b)
       |_->
          match match_with_forall_term env sigma cciterm with
-	     Some (_,a,b)-> Forall (a, b)
-	   |_->
+             Some (_,a,b)-> Forall (a, b)
+           |_->
               match match_with_nodep_ind env sigma cciterm with
-		  Some (i,l,n)->
-		    let ind,u=EConstr.destInd sigma i in
-		    let u = EConstr.EInstance.kind sigma u in
-		    let (mib,mip) = Global.lookup_inductive ind in
-		    let nconstr=Array.length mip.mind_consnames in
-		      if Int.equal nconstr 0 then
-			False((ind,u),l)
-		      else
-			let has_realargs=(n>0) in
-			let is_trivial=
+                  Some (i,l,n)->
+                    let ind,u=EConstr.destInd sigma i in
+                    let u = EConstr.EInstance.kind sigma u in
+                    let (mib,mip) = Global.lookup_inductive ind in
+                    let nconstr=Array.length mip.mind_consnames in
+                      if Int.equal nconstr 0 then
+                        False((ind,u),l)
+                      else
+                        let has_realargs=(n>0) in
+                        let is_trivial=
                           let is_constant n = Int.equal n 0 in
                             Array.exists is_constant mip.mind_consnrealargs in
-			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
-			    (has_realargs && not is_trivial)
-			  then
-			    Atom cciterm
-			  else
-			    if Int.equal nconstr 1 then
-			      And((ind,u),l,is_trivial)
-			    else
-			      Or((ind,u),l,is_trivial)
-		| _ ->
+                          if Inductiveops.mis_is_recursive (ind,mib,mip) ||
+                            (has_realargs && not is_trivial)
+                          then
+                            Atom cciterm
+                          else
+                            if Int.equal nconstr 1 then
+                              And((ind,u),l,is_trivial)
+                            else
+                              Or((ind,u),l,is_trivial)
+                | _ ->
                     match match_with_sigma_type env sigma cciterm with
-			Some (i,l)->
+                        Some (i,l)->
                           let (ind, u) = EConstr.destInd sigma i in
                           let u = EConstr.EInstance.kind sigma u in
                           Exists((ind, u), l)
-		      |_-> Atom (normalize cciterm)
+                      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
 
@@ -132,52 +132,52 @@ let build_atoms env sigma metagen side cciterm =
   let normalize=special_nf env sigma in
   let rec build_rec subst polarity cciterm=
     match kind_of_formula env sigma cciterm with
-	False(_,_)->if not polarity then trivial:=true
+        False(_,_)->if not polarity then trivial:=true
       | Arrow (a,b)->
-	  build_rec subst (not polarity) a;
-	  build_rec subst polarity b
+          build_rec subst (not polarity) a;
+          build_rec subst polarity b
       | And(i,l,b) | Or(i,l,b)->
-	  if b then
-	    begin
-	      let unsigned=normalize (substnl subst 0 cciterm) in
-		if polarity then
-		  positive:= unsigned :: !positive
-		else
-		  negative:= unsigned :: !negative
-	    end;
-	  let v = ind_hyps env sigma 0 i l in
-	  let g i _ decl =
-	    build_rec subst polarity (lift i (RelDecl.get_type decl)) in
-	  let f l =
-	    List.fold_left_i g (1-(List.length l)) () l in
-	    if polarity && (* we have a constant constructor *)
-	      Array.exists (function []->true|_->false) v
-	    then trivial:=true;
-	    Array.iter f v
+          if b then
+            begin
+              let unsigned=normalize (substnl subst 0 cciterm) in
+                if polarity then
+                  positive:= unsigned :: !positive
+                else
+                  negative:= unsigned :: !negative
+            end;
+          let v = ind_hyps env sigma 0 i l in
+          let g i _ decl =
+            build_rec subst polarity (lift i (RelDecl.get_type decl)) in
+          let f l =
+            List.fold_left_i g (1-(List.length l)) () l in
+            if polarity && (* we have a constant constructor *)
+              Array.exists (function []->true|_->false) v
+            then trivial:=true;
+            Array.iter f v
       | Exists(i,l)->
-	  let var=mkMeta (metagen true) in
-	  let v =(ind_hyps env sigma 1 i l).(0) in
-	  let g i _ decl =
-	    build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
-	    List.fold_left_i g (2-(List.length l)) () v
+          let var=mkMeta (metagen true) in
+          let v =(ind_hyps env sigma 1 i l).(0) in
+          let g i _ decl =
+            build_rec (var::subst) polarity (lift i (RelDecl.get_type decl)) in
+            List.fold_left_i g (2-(List.length l)) () v
       | Forall(_,b)->
-	  let var=mkMeta (metagen true) in
-	    build_rec (var::subst) polarity b
+          let var=mkMeta (metagen true) in
+            build_rec (var::subst) polarity b
       | Atom t->
-	  let unsigned=substnl subst 0 t in
-	    if not (isMeta sigma unsigned) then (* discarding wildcard atoms *)
-	      if polarity then
-		positive:= unsigned :: !positive
-	      else
-		negative:= unsigned :: !negative in
+          let unsigned=substnl subst 0 t in
+            if not (isMeta sigma unsigned) then (* discarding wildcard atoms *)
+              if polarity then
+                positive:= unsigned :: !positive
+              else
+                negative:= unsigned :: !negative in
     begin
       match side with
-	  Concl    -> build_rec [] true cciterm
-	| Hyp      -> build_rec [] false cciterm
-	| Hint     ->
-	    let rels,head=decompose_prod sigma cciterm in
-	    let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
-	      build_rec subst false head;trivial:=false (* special for hints *)
+          Concl    -> build_rec [] true cciterm
+        | Hyp      -> build_rec [] false cciterm
+        | Hint     ->
+            let rels,head=decompose_prod sigma cciterm in
+            let subst=List.rev_map (fun _->mkMeta (metagen true)) rels in
+              build_rec subst false head;trivial:=false (* special for hints *)
     end;
     (!trivial,
      {positive= !positive;
@@ -209,65 +209,65 @@ type left_pattern=
   | LA of constr*left_arrow_pattern
 
 type t={id:GlobRef.t;
-	constr:constr;
-	pat:(left_pattern,right_pattern) sum;
-	atoms:atoms}
+        constr:constr;
+        pat:(left_pattern,right_pattern) sum;
+        atoms:atoms}
 
 let build_formula env sigma side nam typ metagen=
   let normalize = special_nf env sigma in
     try
       let m=meta_succ(metagen false) in
       let trivial,atoms=
-	if !qflag then
-	  build_atoms env sigma metagen side typ
-	else no_atoms in
+        if !qflag then
+          build_atoms env sigma metagen side typ
+        else no_atoms in
       let pattern=
-	match side with
-	    Concl ->
-	      let pat=
-		match kind_of_formula env sigma typ with
-		    False(_,_)        -> Rfalse
-		  | Atom a       -> raise (Is_atom a)
-		  | And(_,_,_)        -> Rand
-		  | Or(_,_,_)         -> Ror
-		  | Exists (i,l) ->
-		      let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in
-			Rexists(m,d,trivial)
-		  | Forall (_,a) -> Rforall
-		  | Arrow (a,b) -> Rarrow in
-		Right pat
-	  | _ ->
-	      let pat=
-		match kind_of_formula env sigma typ with
-		    False(i,_)        ->  Lfalse
-		  | Atom a       ->  raise (Is_atom a)
-		  | And(i,_,b)         ->
-		      if b then
-			let nftyp=normalize typ in raise (Is_atom nftyp)
-		      else Land i
-		  | Or(i,_,b)          ->
-		      if b then
-			let nftyp=normalize typ in raise (Is_atom nftyp)
-		      else Lor i
-		  | Exists (ind,_) ->  Lexists ind
-		  | Forall (d,_) ->
-		      Lforall(m,d,trivial)
-		  | Arrow (a,b) ->
-		      let nfa=normalize a in
-			LA (nfa,
-			    match kind_of_formula env sigma a with
-				False(i,l)-> LLfalse(i,l)
-			      | Atom t->     LLatom
-			      | And(i,l,_)-> LLand(i,l)
-			      | Or(i,l,_)->  LLor(i,l)
-			      | Arrow(a,c)-> LLarrow(a,c,b)
-			      | Exists(i,l)->LLexists(i,l)
-			      | Forall(_,_)->LLforall a) in
-		Left pat
+        match side with
+            Concl ->
+              let pat=
+                match kind_of_formula env sigma typ with
+                    False(_,_)        -> Rfalse
+                  | Atom a       -> raise (Is_atom a)
+                  | And(_,_,_)        -> Rand
+                  | Or(_,_,_)         -> Ror
+                  | Exists (i,l) ->
+                      let d = RelDecl.get_type (List.last (ind_hyps env sigma 0 i l).(0)) in
+                        Rexists(m,d,trivial)
+                  | Forall (_,a) -> Rforall
+                  | Arrow (a,b) -> Rarrow in
+                Right pat
+          | _ ->
+              let pat=
+                match kind_of_formula env sigma typ with
+                    False(i,_)        ->  Lfalse
+                  | Atom a       ->  raise (Is_atom a)
+                  | And(i,_,b)         ->
+                      if b then
+                        let nftyp=normalize typ in raise (Is_atom nftyp)
+                      else Land i
+                  | Or(i,_,b)          ->
+                      if b then
+                        let nftyp=normalize typ in raise (Is_atom nftyp)
+                      else Lor i
+                  | Exists (ind,_) ->  Lexists ind
+                  | Forall (d,_) ->
+                      Lforall(m,d,trivial)
+                  | Arrow (a,b) ->
+                      let nfa=normalize a in
+                        LA (nfa,
+                            match kind_of_formula env sigma a with
+                                False(i,l)-> LLfalse(i,l)
+                              | Atom t->     LLatom
+                              | And(i,l,_)-> LLand(i,l)
+                              | Or(i,l,_)->  LLor(i,l)
+                              | Arrow(a,c)-> LLarrow(a,c,b)
+                              | Exists(i,l)->LLexists(i,l)
+                              | Forall(_,_)->LLforall a) in
+                Left pat
       in
-	Left {id=nam;
-	      constr=normalize typ;
-	      pat=pattern;
-	      atoms=atoms}
+        Left {id=nam;
+              constr=normalize typ;
+              pat=pattern;
+              atoms=atoms}
     with Is_atom a-> Right a (* already in nf *)
 
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index dc422fa284..b8a619d1e6 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -66,9 +66,9 @@ type left_pattern=
   | LA of constr*left_arrow_pattern
 
 type t={id: GlobRef.t;
-	constr: constr;
-	pat: (left_pattern,right_pattern) sum;
-	atoms: atoms}
+        constr: constr;
+        pat: (left_pattern,right_pattern) sum;
+        atoms: atoms}
 
 (*exception Is_atom of constr*)
 
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 35cd10a1ff..2bc79d45d4 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -41,7 +41,7 @@ let ()=
       optread=(fun ()->Some !ground_depth);
       optwrite=
    (function
-	None->ground_depth:=3
+        None->ground_depth:=3
       |	Some i->ground_depth:=(max i 0))}
   in
     declare_int_option gdopt
@@ -68,7 +68,7 @@ let default_intuition_tac =
   Tacenv.register_ml_tactic name [| tac |];
   Tacexpr.TacML (CAst.make (entry, []))
 
-let (set_default_solver, default_solver, print_default_solver) = 
+let (set_default_solver, default_solver, print_default_solver) =
   Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
 
 }
@@ -95,12 +95,12 @@ let gen_ground_tac flag taco ids bases =
   Proofview.Goal.enter begin fun gl ->
       qflag:=flag;
       let solver=
-	match taco with
-	    Some tac-> tac
-	  | None-> snd (default_solver ()) in
+        match taco with
+            Some tac-> tac
+          | None-> snd (default_solver ()) in
       let startseq k =
         Proofview.Goal.enter begin fun gl ->
-	let seq=empty_seq !ground_depth in
+        let seq=empty_seq !ground_depth in
         let seq, sigma = extend_with_ref_list (pf_env gl) (project gl) ids seq in
         let seq, sigma = extend_with_auto_hints (pf_env gl) (project gl) bases seq in
         tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k seq)
@@ -124,10 +124,10 @@ let defined_connectives=lazy
 let normalize_evaluables=
   onAllHypsAndConcl
     (function
-	 None->unfold_in_concl (Lazy.force defined_connectives)
+         None->unfold_in_concl (Lazy.force defined_connectives)
        | Some id->
-	   unfold_in_hyp (Lazy.force defined_connectives)
-	   (Tacexpr.InHypType id)) *)
+           unfold_in_hyp (Lazy.force defined_connectives)
+           (Tacexpr.InHypType id)) *)
 
 open Ppconstr
 open Printer
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index e134562702..2f26226f4e 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -41,89 +41,89 @@ let ground_tac solver startseq =
     in
     tclORELSE (axiom_tac seq.gl seq)
       begin
-	try
-	  let (hd,seq1)=take_formula (project gl) seq
-	  and re_add s=re_add_formula_list (project gl) skipped s in
-	  let continue=toptac []
-	  and backtrack =toptac (hd::skipped) seq1 in
-	    match hd.pat with
-		Right rpat->
-		  begin
-		    match rpat with
-			Rand->
-			  and_tac backtrack continue (re_add seq1)
-		      | Rforall->
-			  let backtrack1=
-			    if !qflag then
-			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
-			    else
-			      backtrack in
-			    forall_tac backtrack1 continue (re_add seq1)
-		      | Rarrow->
-			  arrow_tac backtrack continue (re_add seq1)
-		      | Ror->
-			  or_tac  backtrack continue (re_add seq1)
-		      | Rfalse->backtrack
-		      | Rexists(i,dom,triv)->
-			  let (lfp,seq2)=collect_quantified (project gl) seq in
-			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then
-			      quantified_tac lfp backtrack2
-				continue (re_add seq)
-			    else
-			      backtrack2 (* need special backtracking *)
-		  end
-	      | Left lpat->
-		  begin
-		    match lpat with
-			Lfalse->
-			  left_false_tac hd.id
-		      | Land ind->
-			  left_and_tac ind backtrack
-			  hd.id continue (re_add seq1)
-		      | Lor ind->
-			  left_or_tac ind backtrack
-			  hd.id continue (re_add seq1)
-		      | Lforall (_,_,_)->
-			  let (lfp,seq2)=collect_quantified (project gl) seq in
-			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then
-			      quantified_tac lfp backtrack2
-				continue (re_add seq)
-			    else
-			      backtrack2 (* need special backtracking *)
-  		      | Lexists ind ->
-			  if !qflag then
-			    left_exists_tac ind backtrack hd.id
-			      continue (re_add seq1)
-			  else backtrack
-		      | LA (typ,lap)->
-			  let la_tac=
-			    begin
-			      match lap with
-				  LLatom -> backtrack
-				| LLand (ind,largs) | LLor(ind,largs)
-				| LLfalse (ind,largs)->
-				    (ll_ind_tac ind largs backtrack
-				       hd.id continue (re_add seq1))
-				| LLforall p ->
-				    if seq.depth>0 && !qflag then
-				      (ll_forall_tac p backtrack
-					 hd.id continue (re_add seq1))
-				    else backtrack
-				| LLexists (ind,l) ->
-				    if !qflag then
-				      ll_ind_tac ind l backtrack
-					hd.id continue (re_add seq1)
-				    else
-				      backtrack
-				| LLarrow (a,b,c) ->
-				    (ll_arrow_tac a b c backtrack
-				       hd.id continue (re_add seq1))
-			    end in
-			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
-		  end
-	    with Heap.EmptyHeap->solver
+        try
+          let (hd,seq1)=take_formula (project gl) seq
+          and re_add s=re_add_formula_list (project gl) skipped s in
+          let continue=toptac []
+          and backtrack =toptac (hd::skipped) seq1 in
+            match hd.pat with
+                Right rpat->
+                  begin
+                    match rpat with
+                        Rand->
+                          and_tac backtrack continue (re_add seq1)
+                      | Rforall->
+                          let backtrack1=
+                            if !qflag then
+                              tclFAIL 0 (Pp.str "reversible in 1st order mode")
+                            else
+                              backtrack in
+                            forall_tac backtrack1 continue (re_add seq1)
+                      | Rarrow->
+                          arrow_tac backtrack continue (re_add seq1)
+                      | Ror->
+                          or_tac  backtrack continue (re_add seq1)
+                      | Rfalse->backtrack
+                      | Rexists(i,dom,triv)->
+                          let (lfp,seq2)=collect_quantified (project gl) seq in
+                          let backtrack2=toptac (lfp@skipped) seq2 in
+                            if  !qflag && seq.depth>0 then
+                              quantified_tac lfp backtrack2
+                                continue (re_add seq)
+                            else
+                              backtrack2 (* need special backtracking *)
+                  end
+              | Left lpat->
+                  begin
+                    match lpat with
+                        Lfalse->
+                          left_false_tac hd.id
+                      | Land ind->
+                          left_and_tac ind backtrack
+                          hd.id continue (re_add seq1)
+                      | Lor ind->
+                          left_or_tac ind backtrack
+                          hd.id continue (re_add seq1)
+                      | Lforall (_,_,_)->
+                          let (lfp,seq2)=collect_quantified (project gl) seq in
+                          let backtrack2=toptac (lfp@skipped) seq2 in
+                            if  !qflag && seq.depth>0 then
+                              quantified_tac lfp backtrack2
+                                continue (re_add seq)
+                            else
+                              backtrack2 (* need special backtracking *)
+                      | Lexists ind ->
+                          if !qflag then
+                            left_exists_tac ind backtrack hd.id
+                              continue (re_add seq1)
+                          else backtrack
+                      | LA (typ,lap)->
+                          let la_tac=
+                            begin
+                              match lap with
+                                  LLatom -> backtrack
+                                | LLand (ind,largs) | LLor(ind,largs)
+                                | LLfalse (ind,largs)->
+                                    (ll_ind_tac ind largs backtrack
+                                       hd.id continue (re_add seq1))
+                                | LLforall p ->
+                                    if seq.depth>0 && !qflag then
+                                      (ll_forall_tac p backtrack
+                                         hd.id continue (re_add seq1))
+                                    else backtrack
+                                | LLexists (ind,l) ->
+                                    if !qflag then
+                                      ll_ind_tac ind l backtrack
+                                        hd.id continue (re_add seq1)
+                                    else
+                                      backtrack
+                                | LLarrow (a,b,c) ->
+                                    (ll_arrow_tac a b c backtrack
+                                       hd.id continue (re_add seq1))
+                            end in
+                            ll_atom_tac typ la_tac hd.id continue (re_add seq1)
+                  end
+            with Heap.EmptyHeap->solver
       end
     end in
     let n = List.length (Proofview.Goal.hyps gl) in
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eff0db5bf4..e131cad7da 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -26,13 +26,13 @@ open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
         let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
-	match inst1,inst2 with
-	    Phantom(d1),Phantom(d2)->
-	      (cmp d1 d2)
-	  | Real((m1,c1),n1),Real((m2,c2),n2)->
-	      ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
-	  | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
-	  | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
+        match inst1,inst2 with
+            Phantom(d1),Phantom(d2)->
+              (cmp d1 d2)
+          | Real((m1,c1),n1),Real((m2,c2),n2)->
+              ((-) =? (-) ==? cmp) m2 m1 n1 n2 c1 c2
+          | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
+          | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
 
 let compare_gr id1 id2 =
   if id1==id2 then 0 else
@@ -53,7 +53,7 @@ module IS=Set.Make(OrderedInstance)
 let make_simple_atoms seq=
   let ratoms=
     match seq.glatom with
-	Some t->[t]
+        Some t->[t]
       | None->[]
   in {negative=seq.latoms;positive=ratoms}
 
@@ -63,9 +63,9 @@ let do_sequent sigma setref triv id seq i dom atoms=
   let do_atoms a1 a2 =
     let do_pair t1 t2 =
       match unif_atoms sigma i dom t1 t2 with
-	  None->()
-	| Some (Phantom _) ->phref:=true
-	| Some c ->flag:=false;setref:=IS.add (c,id) !setref in
+          None->()
+        | Some (Phantom _) ->phref:=true
+        | Some c ->flag:=false;setref:=IS.add (c,id) !setref in
       List.iter (fun t->List.iter (do_pair t) a2.negative) a1.positive;
       List.iter (fun t->List.iter (do_pair t) a2.positive) a1.negative in
     HP.iter (fun lf->do_atoms atoms lf.atoms) seq.redexes;
@@ -75,8 +75,8 @@ let do_sequent sigma setref triv id seq i dom atoms=
 let match_one_quantified_hyp sigma setref seq lf=
   match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
-	if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
-	  setref:=IS.add ((Phantom dom),lf.id) !setref
+        if do_sequent sigma setref triv lf.id seq i dom lf.atoms then
+          setref:=IS.add ((Phantom dom),lf.id) !setref
     | _ -> anomaly (Pp.str "can't happen.")
 
 let give_instances sigma lf seq=
@@ -90,10 +90,10 @@ let rec collect_quantified sigma seq=
   try
     let hd,seq1=take_formula sigma seq in
       (match hd.pat with
-	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
-	     let (q,seq2)=collect_quantified sigma seq1 in
-	       ((hd::q),seq2)
-	 | _->[],seq)
+           Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
+             let (q,seq2)=collect_quantified sigma seq1 in
+               ((hd::q),seq2)
+         | _->[],seq)
   with Heap.EmptyHeap -> [],seq
 
 (* open instances processor *)
@@ -104,19 +104,19 @@ let mk_open_instance env evmap id idc m t =
   let var_id=
     if id==dummy_id then dummy_bvid else
       let typ=Typing.unsafe_type_of env evmap idc in
-	(* since we know we will get a product,
-	   reduction is not too expensive *)
+        (* since we know we will get a product,
+           reduction is not too expensive *)
       let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
         match nam.Context.binder_name with
-	    Name id -> id
-	  | Anonymous ->  dummy_bvid in
+            Name id -> id
+          | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   let rec aux n avoid env evmap decls =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id_in_env avoid var_id env) in
       let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
       let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
-	aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
+        aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m Id.Set.empty env evmap [] in
   (evmap, decls, revt)
 
@@ -128,49 +128,49 @@ let left_instance_tac (inst,id) continue seq=
   let sigma = project gl in
   match inst with
       Phantom dom->
-	if lookup sigma (id,None) seq then
-	  tclFAIL 0 (Pp.str "already done")
-	else
-	  tclTHENS (cut dom)
-	    [tclTHENLIST
-	       [introf;
+        if lookup sigma (id,None) seq then
+          tclFAIL 0 (Pp.str "already done")
+        else
+          tclTHENS (cut dom)
+            [tclTHENLIST
+               [introf;
                 (pf_constr_of_global id >>= fun idc ->
                 Proofview.Goal.enter begin fun gl ->
                   let id0 = List.nth (pf_ids_of_hyps gl) 0 in
                   generalize [mkApp(idc, [|mkVar id0|])]
                 end);
-		introf;
-		tclSOLVE [wrap 1 false continue
-			    (deepen (record (id,None) seq))]];
-	    tclTRY assumption]
+                introf;
+                tclSOLVE [wrap 1 false continue
+                            (deepen (record (id,None) seq))]];
+            tclTRY assumption]
     | Real((m,t),_)->
         let c = (m, EConstr.to_constr sigma t) in
-	if lookup sigma (id,Some c) seq then
-	  tclFAIL 0 (Pp.str "already done")
-	else
-	  let special_generalize=
-	    if m>0 then
-	      (pf_constr_of_global id >>= fun idc ->
-		Proofview.Goal.enter begin fun gl->
-		  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
-		  let gt=
-		    it_mkLambda_or_LetIn
-		      (mkApp(idc,[|ot|])) rc in
-		  let evmap, _ =
-		    try Typing.type_of (pf_env gl) evmap gt
-		    with e when CErrors.noncritical e ->
-		      user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
+        if lookup sigma (id,Some c) seq then
+          tclFAIL 0 (Pp.str "already done")
+        else
+          let special_generalize=
+            if m>0 then
+              (pf_constr_of_global id >>= fun idc ->
+                Proofview.Goal.enter begin fun gl->
+                  let (evmap, rc, ot) = mk_open_instance (pf_env gl) (project gl) id idc m t in
+                  let gt=
+                    it_mkLambda_or_LetIn
+                      (mkApp(idc,[|ot|])) rc in
+                  let evmap, _ =
+                    try Typing.type_of (pf_env gl) evmap gt
+                    with e when CErrors.noncritical e ->
+                      user_err Pp.(str "Untypable instance, maybe higher-order non-prenex quantification") in
                   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evmap)
-		    (generalize [gt])
+                    (generalize [gt])
                 end)
-	    else
-	      pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
-	  in
-	    tclTHENLIST
-	      [special_generalize;
-	       introf;
-	       tclSOLVE
-		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
+            else
+              pf_constr_of_global id >>= fun idc -> generalize [mkApp(idc,[|t|])]
+          in
+            tclTHENLIST
+              [special_generalize;
+               introf;
+               tclSOLVE
+                 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
   end
 
 let right_instance_tac inst continue seq=
@@ -178,20 +178,20 @@ let right_instance_tac inst continue seq=
   Proofview.Goal.enter begin fun gl ->
   match inst with
       Phantom dom ->
-	tclTHENS (cut dom)
-	[tclTHENLIST
-	   [introf;
+        tclTHENS (cut dom)
+        [tclTHENLIST
+           [introf;
             Proofview.Goal.enter begin fun gl ->
               let id0 = List.nth (pf_ids_of_hyps gl) 0 in
               split (Tactypes.ImplicitBindings [mkVar id0])
             end;
-	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY assumption]
+            tclSOLVE [wrap 0 true continue (deepen seq)]];
+         tclTRY assumption]
     | Real ((0,t),_) ->
         (tclTHEN (split (Tactypes.ImplicitBindings [t]))
-	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
+           (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
-	tclFAIL 0 (Pp.str "not implemented ... yet")
+        tclFAIL 0 (Pp.str "not implemented ... yet")
   end
 
 let instance_tac inst=
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 79386f7ac9..3413db930b 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -40,13 +40,13 @@ let wrap n b continue seq =
   let rec aux i nc ctx=
     if i<=0 then seq else
       match nc with
-	  []->anomaly (Pp.str "Not the expected number of hyps.")
-	| nd::q->
+          []->anomaly (Pp.str "Not the expected number of hyps.")
+        | nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env sigma id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env sigma id) ctx then
-		(aux (i-1) q (nd::ctx))
-	    else
+            if occur_var env sigma id (pf_concl gls) ||
+              List.exists (occur_var_in_decl env sigma id) ctx then
+                (aux (i-1) q (nd::ctx))
+            else
               add_formula env sigma Hyp (GlobRef.VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) in
   let seq1=aux n nc [] in
   let seq2=if b then
@@ -72,17 +72,17 @@ let ll_atom_tac a backtrack id continue seq =
   let open EConstr in
   tclIFTHENELSE
       (tclTHENLIST
-	[(Proofview.tclEVARMAP >>= fun sigma ->
+        [(Proofview.tclEVARMAP >>= fun sigma ->
           let gr =
             try Proofview.tclUNIT (find_left sigma a seq)
             with Not_found -> tclFAIL 0 (Pp.str "No link")
           in
           gr >>= fun gr ->
           pf_constr_of_global gr >>= fun left ->
-	  pf_constr_of_global id >>= fun id -> 
-	    generalize [(mkApp(id, [|left|]))]);
-	 clear_global id;
-	 intro])
+          pf_constr_of_global id >>= fun id ->
+            generalize [(mkApp(id, [|left|]))]);
+         clear_global id;
+         intro])
     (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
@@ -151,12 +151,12 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
          EConstr.it_mkLambda_or_LetIn head rc in
        let lp=Array.length rcs in
        let newhyps idc =List.init lp (myterm idc) in
-	 tclIFTHENELSE
-	   (tclTHENLIST
-	      [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc));
-	       clear_global id;
-	       tclDO lp intro])
-	   (wrap lp false continue seq) backtrack
+         tclIFTHENELSE
+           (tclTHENLIST
+              [(pf_constr_of_global id >>= fun idc -> generalize (newhyps idc));
+               clear_global id;
+               tclDO lp intro])
+           (wrap lp false continue seq) backtrack
   end
 
 let ll_arrow_tac a b c backtrack id continue seq=
@@ -167,18 +167,18 @@ let ll_arrow_tac a b c backtrack id continue seq=
                   mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (cut c)
-	 [tclTHENLIST
-	    [introf;
-	     clear_global id;
-	     wrap 1 false continue seq];
-	  tclTHENS (cut cc)
+         [tclTHENLIST
+            [introf;
+             clear_global id;
+             wrap 1 false continue seq];
+          tclTHENS (cut cc)
             [(pf_constr_of_global id >>= fun c -> exact_no_check c);
-	     tclTHENLIST
-	       [(pf_constr_of_global id >>= fun idc -> generalize [d idc]);
-		clear_global id;
-		introf;
-		introf;
-		tclCOMPLETE (wrap 2 true continue seq)]]])
+             tclTHENLIST
+               [(pf_constr_of_global id >>= fun idc -> generalize [d idc]);
+                clear_global id;
+                introf;
+                introf;
+                tclCOMPLETE (wrap 2 true continue seq)]]])
       backtrack
 
 (* quantifier rules (easy side) *)
@@ -187,8 +187,8 @@ let forall_tac backtrack continue seq=
   tclORELSE
     (tclIFTHENELSE intro (wrap 0 true continue seq)
        (tclORELSE
-	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
-	  backtrack))
+          (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
+          backtrack))
     (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
@@ -209,18 +209,18 @@ let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
     (tclTHENS (cut prod)
        [tclTHENLIST
-	  [intro;
+          [intro;
            (pf_constr_of_global id >>= fun idc ->
-	   Proofview.Goal.enter begin fun gls->
+           Proofview.Goal.enter begin fun gls->
               let open EConstr in
-	      let id0 = List.nth (pf_ids_of_hyps gls) 0 in
+              let id0 = List.nth (pf_ids_of_hyps gls) 0 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
               tclTHEN (generalize [term]) (clear [id0])
            end);
-	   clear_global id;
-	   intro;
-	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
-	tclCOMPLETE (wrap 0 true continue (deepen seq))])
+           clear_global id;
+           intro;
+           tclCOMPLETE (wrap 1 false continue (deepen seq))];
+        tclCOMPLETE (wrap 0 true continue (deepen seq))])
     backtrack
 
 (* rules for instantiation with unification moved to instances.ml *)
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 "-----"))
 
 
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 724e1abcc4..2e262fd996 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -28,12 +28,12 @@ module HP: Heap.S with type elt=Formula.t
 
 type t = {redexes:HP.t;
           context: GlobRef.t list CM.t;
-	  latoms:constr list;
-	  gl:types;
-	  glatom:constr option;
-	  cnt:counter;
-	  history:History.t;
-	  depth:int}
+          latoms:constr list;
+          gl:types;
+          glatom:constr option;
+          cnt:counter;
+          history:History.t;
+          depth:int}
 
 val deepen: t -> t
 
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