Delete trailing whitespaces in all *.{v,ml*} files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 255 insertions, 255 deletions

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 0be3a4b39..45365cb2c 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -41,20 +41,20 @@ let meta_succ m = m+1
 
 let rec nb_prod_after n c=
   match kind_of_term c with
-    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else 
+    | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
 	1+(nb_prod_after 0 b)
     | _ -> 0
 
 let construct_nhyps ind gls =
   let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
-  let hyp = nb_prod_after nparams in	
+  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let hyp = nb_prod_after nparams in
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
-let ind_hyps nevar ind largs gls= 
-  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in 
-  let lp=Array.length types in     
+let ind_hyps nevar ind largs gls=
+  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
+  let lp=Array.length types in
   let myhyps i=
     let t1=Term.prod_applist types.(i) largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
@@ -77,7 +77,7 @@ type kind_of_formula=
   | Exists of inductive*constr list
   | Forall of constr*constr
   | Atom of constr
-      
+
 let rec kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
@@ -86,34 +86,34 @@ let rec kind_of_formula gl term =
       |_->
 	 match match_with_forall_term cciterm with
 	     Some (_,a,b)-> Forall(a,b)
-	   |_-> 
+	   |_->
 	      match match_with_nodep_ind cciterm with
 		  Some (i,l,n)->
 		    let ind=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
-		      if nconstr=0 then 
+		      if nconstr=0 then
 			False(ind,l)
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mib.mind_nparams in  
-			    array_exists is_constant mip.mind_nf_lc in 
+			    nb_prod c = mib.mind_nparams in
+			    array_exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
 			  then
-			    Atom cciterm 
+			    Atom cciterm
 			  else
 			    if nconstr=1 then
 			      And(ind,l,is_trivial)
-			    else 
-			      Or(ind,l,is_trivial) 
-		| _ ->  
+			    else
+			      Or(ind,l,is_trivial)
+		| _ ->
 		    match match_with_sigma_type cciterm with
 			Some (i,l)-> Exists((destInd i),l)
 		      |_-> Atom (normalize cciterm)
-  
+
 type atoms = {positive:constr list;negative:constr list}
 
 type side = Hyp | Concl | Hint
@@ -126,7 +126,7 @@ let build_atoms gl metagen side cciterm =
   let trivial =ref false
   and positive=ref []
   and negative=ref [] in
-  let normalize=special_nf gl in 
+  let normalize=special_nf gl in
   let rec build_rec env polarity cciterm=
     match kind_of_formula gl cciterm with
 	False(_,_)->if not polarity then trivial:=true
@@ -134,12 +134,12 @@ let build_atoms gl metagen side cciterm =
 	  build_rec env (not polarity) a;
 	  build_rec env polarity b
       | And(i,l,b) | Or(i,l,b)->
-	  if b then 
+	  if b then
 	    begin
 	      let unsigned=normalize (substnl env 0 cciterm) in
-		if polarity then 
-		  positive:= unsigned :: !positive 
-		else 
+		if polarity then
+		  positive:= unsigned :: !positive
+		else
 		  negative:= unsigned :: !negative
 	    end;
 	  let v = ind_hyps 0 i l gl in
@@ -148,9 +148,9 @@ let build_atoms gl metagen side cciterm =
 	  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 
+	      array_exists (function []->true|_->false) v
 	    then trivial:=true;
-	    Array.iter f v 
+	    Array.iter f v
       | Exists(i,l)->
 	  let var=mkMeta (metagen true) in
 	  let v =(ind_hyps 1 i l gl).(0) in
@@ -163,15 +163,15 @@ let build_atoms gl metagen side cciterm =
       | Atom t->
 	  let unsigned=substnl env 0 t in
 	    if not (isMeta unsigned) then (* discarding wildcard atoms *)
-	      if polarity then 
-		positive:= unsigned :: !positive 
-	      else 
+	      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     -> 
+	| Hint     ->
 	    let rels,head=decompose_prod cciterm in
 	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
 	      build_rec env false head;trivial:=false (* special for hints *)
@@ -179,15 +179,15 @@ let build_atoms gl metagen side cciterm =
     (!trivial,
      {positive= !positive;
       negative= !negative})
-    
+
 type right_pattern =
     Rarrow
   | Rand
-  | Ror 
+  | Ror
   | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-   
+
 type left_arrow_pattern=
     LLatom
   | LLfalse of inductive*constr list
@@ -198,9 +198,9 @@ type left_arrow_pattern=
   | LLarrow of constr*constr*constr
 
 type left_pattern=
-    Lfalse    
+    Lfalse
   | Land of inductive
-  | Lor of inductive 
+  | Lor of inductive
   | Lforall of metavariable*constr*bool
   | Lexists of inductive
   | LA of constr*left_arrow_pattern
@@ -209,14 +209,14 @@ type t={id:global_reference;
 	constr:constr;
 	pat:(left_pattern,right_pattern) sum;
 	atoms:atoms}
-    
+
 let build_formula side nam typ gl metagen=
   let normalize = special_nf gl in
-    try 
+    try
       let m=meta_succ(metagen false) in
       let trivial,atoms=
-	if !qflag then 
-	  build_atoms gl metagen side typ 
+	if !qflag then
+	  build_atoms gl metagen side typ
 	else no_atoms in
       let pattern=
 	match side with
@@ -227,10 +227,10 @@ let build_formula side nam typ gl metagen=
 		  | Atom a       -> raise (Is_atom a)
 		  | And(_,_,_)        -> Rand
 		  | Or(_,_,_)         -> Ror
-		  | Exists (i,l) -> 
+		  | Exists (i,l) ->
 		      let (_,_,d)=list_last (ind_hyps 0 i l gl).(0) in
 			Rexists(m,d,trivial)
-		  | Forall (_,a) -> Rforall 
+		  | Forall (_,a) -> Rforall
 		  | Arrow (a,b) -> Rarrow in
 		Right pat
 	  | _ ->
@@ -238,7 +238,7 @@ let build_formula side nam typ gl metagen=
 		match kind_of_formula gl typ with
 		    False(i,_)        ->  Lfalse
 		  | Atom a       ->  raise (Is_atom a)
-		  | And(i,_,b)         ->  
+		  | And(i,_,b)         ->
 		      if b then
 			let nftyp=normalize typ in raise (Is_atom nftyp)
 		      else Land i
@@ -246,12 +246,12 @@ let build_formula side nam typ gl metagen=
 		      if b then
 			let nftyp=normalize typ in raise (Is_atom nftyp)
 		      else Lor i
-		  | Exists (ind,_) ->  Lexists ind 
-		  | Forall (d,_) -> 
+		  | Exists (ind,_) ->  Lexists ind
+		  | Forall (d,_) ->
 		      Lforall(m,d,trivial)
 		  | Arrow (a,b) ->
 		      let nfa=normalize a in
-			LA (nfa, 
+			LA (nfa,
 			    match kind_of_formula gl a with
 				False(i,l)-> LLfalse(i,l)
 			      | Atom t->     LLatom
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 9e9d1e122..2e89ddb06 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -16,10 +16,10 @@ val qflag : bool ref
 
 val red_flags: Closure.RedFlags.reds ref
 
-val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 
+val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
-  
-val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) -> 
+
+val (==?) : ('a -> 'a -> 'b ->'b -> int) -> ('c -> 'c -> int) ->
   'a -> 'a -> 'b -> 'b -> 'c ->'c -> int
 
 type ('a,'b) sum = Left of 'a | Right of 'b
@@ -28,7 +28,7 @@ type counter = bool -> metavariable
 
 val construct_nhyps : inductive -> Proof_type.goal Tacmach.sigma -> int array
 
-val ind_hyps : int -> inductive -> constr list -> 
+val ind_hyps : int -> inductive -> constr list ->
   Proof_type.goal Tacmach.sigma -> rel_context array
 
 type atoms = {positive:constr list;negative:constr list}
@@ -36,18 +36,18 @@ type atoms = {positive:constr list;negative:constr list}
 type side = Hyp | Concl | Hint
 
 val dummy_id: global_reference
-			
-val build_atoms : Proof_type.goal Tacmach.sigma -> counter -> 
+
+val build_atoms : Proof_type.goal Tacmach.sigma -> counter ->
   side -> constr -> bool * atoms
 
 type right_pattern =
     Rarrow
   | Rand
-  | Ror 
+  | Ror
   | Rfalse
   | Rforall
   | Rexists of metavariable*constr*bool
-    
+
 type left_arrow_pattern=
     LLatom
   | LLfalse of inductive*constr list
@@ -58,20 +58,20 @@ type left_arrow_pattern=
   | LLarrow of constr*constr*constr
 
 type left_pattern=
-    Lfalse    
+    Lfalse
   | Land of inductive
-  | Lor of inductive 
+  | Lor of inductive
   | Lforall of metavariable*constr*bool
   | Lexists of inductive
   | LA of constr*left_arrow_pattern
-      
+
 type t={id: global_reference;
 	constr: constr;
 	pat: (left_pattern,right_pattern) sum;
 	atoms: atoms}
-    
+
 (*exception Is_atom of constr*)
 
-val build_formula : side -> global_reference -> types -> 
+val build_formula : side -> global_reference -> types ->
   Proof_type.goal Tacmach.sigma -> counter -> (t,types) sum
 
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 8302da5c1..c986a3026 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -30,10 +30,10 @@ let _=
   let gdopt=
     { optsync=true;
       optname="Firstorder Depth";
-      optkey=["Firstorder";"Depth"]; 
-      optread=(fun ()->Some !ground_depth); 
+      optkey=["Firstorder";"Depth"];
+      optread=(fun ()->Some !ground_depth);
       optwrite=
-   (function 
+   (function
 	None->ground_depth:=3
       |	Some i->ground_depth:=(max i 0))}
   in
@@ -45,10 +45,10 @@ let _=
   let gdopt=
     { optsync=true;
       optname="Congruence Depth";
-      optkey=["Congruence";"Depth"]; 
-      optread=(fun ()->Some !congruence_depth); 
+      optkey=["Congruence";"Depth"];
+      optread=(fun ()->Some !congruence_depth);
       optwrite=
-   (function 
+   (function
 	None->congruence_depth:=0
       |	Some i->congruence_depth:=(max i 0))}
   in
@@ -57,23 +57,23 @@ let _=
 let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
 
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
-		      
+
 let gen_ground_tac flag taco ids bases gl=
   let backup= !qflag in
     try
       qflag:=flag;
-      let solver= 
-	match taco with 
+      let solver=
+	match taco with
 	    Some tac-> tac
 	  | None-> default_solver in
       let startseq gl=
 	let seq=empty_seq !ground_depth in
 	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
-      let result=ground_tac solver startseq gl in 
+      let result=ground_tac solver startseq gl in
 	qflag:=backup;result
     with e ->qflag:=backup;raise e
-      
-(* special for compatibility with Intuition 
+
+(* special for compatibility with Intuition
 
 let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str
 
@@ -83,10 +83,10 @@ let defined_connectives=lazy
 
 let normalize_evaluables=
   onAllHypsAndConcl
-    (function 
+    (function
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some id-> 
-	   unfold_in_hyp (Lazy.force defined_connectives) 
+       | Some id->
+	   unfold_in_hyp (Lazy.force defined_connectives)
 	   (Tacexpr.InHypType id)) *)
 
 open Genarg
@@ -116,12 +116,12 @@ END
 TACTIC EXTEND firstorder
     [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) l [] ]
-|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> 
+|   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) [] l ]
-|   [ "firstorder" tactic_opt(t) firstorder_using(l) 
-       "with" ne_preident_list(l') ] -> 
+|   [ "firstorder" tactic_opt(t) firstorder_using(l)
+       "with" ne_preident_list(l') ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
-|   [ "firstorder" tactic_opt(t) ] -> 
+|   [ "firstorder" tactic_opt(t) ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
 END
 
@@ -131,11 +131,11 @@ TACTIC EXTEND gintuition
 END
 
 
-let default_declarative_automation gls = 
+let default_declarative_automation gls =
   tclORELSE
-    (tclORELSE (Auto.h_trivial [] None) 
+    (tclORELSE (Auto.h_trivial [] None)
     (Cctac.congruence_tac !congruence_depth []))
-    (gen_ground_tac true 
+    (gen_ground_tac true
        (Some (tclTHEN
 		default_solver
 		(Cctac.congruence_tac !congruence_depth [])))
@@ -143,6 +143,6 @@ let default_declarative_automation gls =
 
 
 
-let () = 
+let () =
   Decl_proof_instr.register_automation_tac default_declarative_automation
 
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index a8d5fc2ef..8a0f02d27 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -19,10 +19,10 @@ open Tacticals
 open Libnames
 
 (*
-let old_search=ref !Auto.searchtable 
+let old_search=ref !Auto.searchtable
 
-(* I use this solution as a means to know whether hints have changed, 
-but this prevents the GC from collecting the previous table, 
+(* I use this solution as a means to know whether hints have changed,
+but this prevents the GC from collecting the previous table,
 resulting in some limited space wasting*)
 
 let update_flags ()=
@@ -30,7 +30,7 @@ let update_flags ()=
     begin
       old_search:=!Auto.searchtable;
       let predref=ref Names.KNpred.empty in
-      let f p_a_t = 
+      let f p_a_t =
 	match p_a_t.Auto.code with
 	    Auto.Unfold_nth (ConstRef kn)->
 	      predref:=Names.KNpred.add kn !predref
@@ -39,7 +39,7 @@ let update_flags ()=
       let h _ hdb=Auto.Hint_db.iter g hdb in
 	Util.Stringmap.iter h !Auto.searchtable;
 	red_flags:=
-	Closure.RedFlags.red_add_transparent 
+	Closure.RedFlags.red_add_transparent
 	  Closure.betaiotazeta (Names.Idpred.full,!predref)
     end
 *)
@@ -53,8 +53,8 @@ let update_flags ()=
     with Invalid_argument "destConst"-> () in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent 
-      Closure.betaiotazeta 
+    Closure.RedFlags.red_add_transparent
+      Closure.betaiotazeta
       (Names.Idpred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
@@ -64,10 +64,10 @@ let ground_tac solver startseq gl=
     then Pp.msgnl (Printer.pr_goal (sig_it gl));
     tclORELSE (axiom_tac seq.gl seq)
       begin
-	try      
-	  let (hd,seq1)=take_formula seq  
+	try
+	  let (hd,seq1)=take_formula seq
 	  and re_add s=re_add_formula_list skipped s in
-	  let continue=toptac [] 
+	  let continue=toptac []
 	  and backtrack gl=toptac (hd::skipped) seq1 gl in
 	    match hd.pat with
 		Right rpat->
@@ -77,7 +77,7 @@ let ground_tac solver startseq gl=
 			  and_tac backtrack continue (re_add seq1)
 		      | Rforall->
 			  let backtrack1=
-			    if !qflag then 
+			    if !qflag then
 			      tclFAIL 0 (Pp.str "reversible in 1st order mode")
 			    else
 			      backtrack in
@@ -86,12 +86,12 @@ let ground_tac solver startseq gl=
 			  arrow_tac backtrack continue (re_add seq1)
 		      | Ror->
 			  or_tac  backtrack continue (re_add seq1)
-		      | Rfalse->backtrack 
+		      | Rfalse->backtrack
 		      | Rexists(i,dom,triv)->
 			  let (lfp,seq2)=collect_quantified seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
 				continue (re_add seq)
 			    else
 			      backtrack2 (* need special backtracking *)
@@ -102,21 +102,21 @@ let ground_tac solver startseq gl=
 			Lfalse->
 			  left_false_tac hd.id
 		      | Land ind->
-			  left_and_tac ind backtrack 
+			  left_and_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lor ind->
-			  left_or_tac ind backtrack 
+			  left_or_tac ind backtrack
 			  hd.id continue (re_add seq1)
 		      | Lforall (_,_,_)->
 			  let (lfp,seq2)=collect_quantified seq in
 			  let backtrack2=toptac (lfp@skipped) seq2 in
-			    if  !qflag && seq.depth>0 then 
-			      quantified_tac lfp backtrack2 
+			    if  !qflag && seq.depth>0 then
+			      quantified_tac lfp backtrack2
 				continue (re_add seq)
 			    else
 			      backtrack2 (* need special backtracking *)
   		      | Lexists ind ->
-			  if !qflag then 
+			  if !qflag then
 			    left_exists_tac ind backtrack hd.id
 			      continue (re_add seq1)
 			  else backtrack
@@ -124,14 +124,14 @@ let ground_tac solver startseq gl=
 			  let la_tac=
 			    begin
 			      match lap with
-				  LLatom -> backtrack 
-				| LLand (ind,largs) | LLor(ind,largs) 
+				  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 
+				    (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) ->
@@ -140,13 +140,13 @@ let ground_tac solver startseq gl=
 					hd.id continue (re_add seq1)
 				    else
 				      backtrack
-				| LLarrow (a,b,c) ->	      
+				| LLarrow (a,b,c) ->
 				    (ll_arrow_tac a b c backtrack
 				       hd.id continue (re_add seq1))
-			    end in			 
+			    end in
 			    ll_atom_tac typ la_tac hd.id continue (re_add seq1)
 		  end
 	    with Heap.EmptyHeap->solver
       end gl in
     wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
-      
+
diff --git a/plugins/firstorder/ground_plugin.mllib b/plugins/firstorder/ground_plugin.mllib
index 1647e0f3d..447a1fb51 100644
--- a/plugins/firstorder/ground_plugin.mllib
+++ b/plugins/firstorder/ground_plugin.mllib
@@ -3,6 +3,6 @@ Unify
 Sequent
 Rules
 Instances
-Ground 
+Ground
 G_ground
 Ground_plugin_mod
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 3e087cd8b..810262a69 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -37,8 +37,8 @@ let compare_instance inst1 inst2=
 
 let compare_gr id1 id2=
   if id1==id2 then 0 else
-    if id1==dummy_id then 1 
-    else if id2==dummy_id then -1 
+    if id1==dummy_id then 1
+    else if id2==dummy_id then -1
     else Pervasives.compare id1 id2
 
 module OrderedInstance=
@@ -48,7 +48,7 @@ struct
     (compare_instance =? compare_gr) inst2 inst1 id2 id1
     (* we want a __decreasing__ total order *)
 end
-  
+
 module IS=Set.Make(OrderedInstance)
 
 let make_simple_atoms seq=
@@ -62,7 +62,7 @@ let do_sequent setref triv id seq i dom atoms=
   let flag=ref true in
   let phref=ref triv in
   let do_atoms a1 a2 =
-    let do_pair t1 t2 = 
+    let do_pair t1 t2 =
       match unif_atoms i dom t1 t2 with
 	  None->()
 	| Some (Phantom _) ->phref:=true
@@ -71,27 +71,27 @@ let do_sequent setref triv id seq i dom atoms=
       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;
     do_atoms atoms (make_simple_atoms seq);
-    !flag && !phref 
- 
+    !flag && !phref
+
 let match_one_quantified_hyp setref seq lf=
-  match lf.pat with 
+  match lf.pat with
       Left(Lforall(i,dom,triv))|Right(Rexists(i,dom,triv))->
 	if do_sequent setref triv lf.id seq i dom lf.atoms then
-	  setref:=IS.add ((Phantom dom),lf.id) !setref 
-    | _ ->anomaly "can't happen" 
+	  setref:=IS.add ((Phantom dom),lf.id) !setref
+    | _ ->anomaly "can't happen"
 
 let give_instances lf seq=
   let setref=ref IS.empty in
     List.iter (match_one_quantified_hyp setref seq) lf;
     IS.elements !setref
-	  	  
+
 (* collector for the engine *)
 
 let rec collect_quantified seq=
   try
     let hd,seq1=take_formula seq in
-      (match hd.pat with 
-	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) -> 
+      (match hd.pat with
+	   Left(Lforall(_,_,_)) | Right(Rexists(_,_,_)) ->
 	     let (q,seq2)=collect_quantified seq1 in
 	       ((hd::q),seq2)
 	 | _->[],seq)
@@ -109,10 +109,10 @@ let mk_open_instance id gl m t=
   let var_id=
     if id==dummy_id then dummy_bvid else
       let typ=pf_type_of gl (constr_of_global id) in
-	(* since we know we will get a product, 
+	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
-	match nam with 
+	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (list_tabulate (fun i->mkRel (m-i)) m) t in
@@ -123,15 +123,15 @@ let mk_open_instance id gl m t=
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
   let rawt=Detyping.detype false [] [] nt in
   let rec raux n t=
-    if n=0 then t else 
+    if n=0 then t else
       match t with
 	  RLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
 	      RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1)
 	| _-> anomaly "can't happen" in
-  let ntt=try 
+  let ntt=try
     Pretyping.Default.understand evmap env (raux m rawt)
-  with _ -> 
+  with _ ->
     error "Untypable instance, maybe higher-order non-prenex quantification" in
     decompose_lam_n_assum m ntt
 
@@ -140,51 +140,51 @@ let mk_open_instance id gl m t=
 let left_instance_tac (inst,id) continue seq=
   match inst with
       Phantom dom->
-	if lookup (id,None) seq then 
+	if lookup (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (cut dom) 
+	  tclTHENS (cut dom)
 	    [tclTHENLIST
 	       [introf;
-		(fun gls->generalize 
+		(fun gls->generalize
 		   [mkApp(constr_of_global id,
 			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
 		introf;
-		tclSOLVE [wrap 1 false continue 
+		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
 	    tclTRY assumption]
     | Real((m,t) as c,_)->
-	if lookup (id,Some c) seq then 
+	if lookup (id,Some c) seq then
 	  tclFAIL 0 (Pp.str "already done")
-	else 
+	else
 	  let special_generalize=
-	    if m>0 then 
-	      fun gl-> 
+	    if m>0 then
+	      fun gl->
 		let (rc,ot)= mk_open_instance id gl m t in
-		let gt= 
-		  it_mkLambda_or_LetIn 
+		let gt=
+		  it_mkLambda_or_LetIn
 		    (mkApp(constr_of_global id,[|ot|])) rc in
 		  generalize [gt] gl
 	    else
 	      generalize [mkApp(constr_of_global id,[|t|])]
 	  in
-	    tclTHENLIST 
+	    tclTHENLIST
 	      [special_generalize;
-	       introf; 
-	       tclSOLVE 
+	       introf;
+	       tclSOLVE
 		 [wrap 1 false continue (deepen (record (id,Some c) seq))]]
-	      
+
 let right_instance_tac inst continue seq=
   match inst with
       Phantom dom ->
-	tclTHENS (cut dom) 
+	tclTHENS (cut dom)
 	[tclTHENLIST
 	   [introf;
 	    (fun gls->
-	       split (Rawterm.ImplicitBindings 
+	       split (Rawterm.ImplicitBindings
 			[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
-	 tclTRY assumption] 
+	 tclTRY assumption]
     | Real ((0,t),_) ->
 	(tclTHEN (split (Rawterm.ImplicitBindings [t]))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
@@ -192,7 +192,7 @@ let right_instance_tac inst continue seq=
 	tclFAIL 0 (Pp.str "not implemented ... yet")
 
 let instance_tac inst=
-  if (snd inst)==dummy_id then 
+  if (snd inst)==dummy_id then
     right_instance_tac (fst inst)
   else
     left_instance_tac inst
@@ -203,4 +203,4 @@ let quantified_tac lf backtrack continue seq gl=
       (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
       backtrack gl
 
- 
+
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index aed2ec83d..95dd22ea8 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -13,10 +13,10 @@ open Tacmach
 open Names
 open Libnames
 open Rules
-  
+
 val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
 
-val give_instances : Formula.t list -> Sequent.t -> 
+val give_instances : Formula.t list -> Sequent.t ->
   (Unify.instance * global_reference) list
 
 val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 75d69099a..515efea70 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -31,17 +31,17 @@ let wrap n b continue seq gls=
   let nc=pf_hyps gls in
   let env=pf_env gls in
   let rec aux i nc ctx=
-    if i<=0 then seq else 
+    if i<=0 then seq else
       match nc with
 	  []->anomaly "Not the expected number of hyps"
-	| ((id,_,typ) as nd)::q->  
-	    if occur_var env id (pf_concl gls) || 
+	| ((id,_,typ) as nd)::q->
+	    if occur_var env id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
-  let seq2=if b then 
+  let seq2=if b then
     add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
     continue seq2 gls
 
@@ -52,24 +52,24 @@ let basename_of_global=function
 let clear_global=function
     VarRef id->clear [id]
   | _->tclIDTAC
-      
+
 
 (* connection rules *)
 
 let axiom_tac t seq=
-  try exact_no_check (constr_of_global (find_left t seq)) 
+  try exact_no_check (constr_of_global (find_left t seq))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
-let ll_atom_tac a backtrack id continue seq= 
+let ll_atom_tac a backtrack id continue seq=
   tclIFTHENELSE
-    (try 
+    (try
       tclTHENLIST
 	[generalize [mkApp(constr_of_global id,
 			   [|constr_of_global (find_left a seq)|])];
 	 clear_global id;
 	 intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
-    (wrap 1 false continue seq) backtrack 
+    (wrap 1 false continue seq) backtrack
 
 (* right connectives rules *)
 
@@ -77,7 +77,7 @@ let and_tac backtrack continue seq=
   tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
 
 let or_tac backtrack continue seq=
-  tclORELSE 
+  tclORELSE
     (any_constructor false (Some (tclCOMPLETE (wrap 0 true continue seq))))
     backtrack
 
@@ -89,17 +89,17 @@ let arrow_tac backtrack continue seq=
 (* left connectives rules *)
 
 let left_and_tac ind backtrack id continue seq gls=
- let n=(construct_nhyps ind gls).(0) in  
+ let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
-     (tclTHENLIST 
+     (tclTHENLIST
       [simplest_elim (constr_of_global id);
-       clear_global id; 
+       clear_global id;
        tclDO n intro])
      (wrap n false continue seq)
      backtrack gls
 
 let left_or_tac ind backtrack id continue seq gls=
-  let v=construct_nhyps ind gls in  
+  let v=construct_nhyps ind gls in
   let f n=
     tclTHENLIST
       [clear_global id;
@@ -117,10 +117,10 @@ let left_false_tac id=
 
 (* We use this function for false, and, or, exists *)
 
-let ll_ind_tac ind largs backtrack id continue seq gl= 
+let ll_ind_tac ind largs backtrack id continue seq gl=
      let rcs=ind_hyps 0 ind largs gl in
      let vargs=Array.of_list largs in
-	     (* construire le terme  H->B, le generaliser etc *)   
+	     (* construire le terme  H->B, le generaliser etc *)
      let myterm i=
        let rc=rcs.(i) in
        let p=List.length rc in
@@ -132,7 +132,7 @@ let ll_ind_tac ind largs backtrack id continue seq gl=
        let lp=Array.length rcs in
        let newhyps=list_tabulate myterm lp in
 	 tclIFTHENELSE
-	   (tclTHENLIST 
+	   (tclTHENLIST
 	      [generalize newhyps;
 	       clear_global id;
 	       tclDO lp intro])
@@ -149,9 +149,9 @@ let ll_arrow_tac a b c backtrack id continue seq=
 	    [introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (cut cc) 
-            [exact_no_check (constr_of_global id); 
-	     tclTHENLIST 
+	  tclTHENS (cut cc)
+            [exact_no_check (constr_of_global id);
+	     tclTHENLIST
 	       [generalize [d];
 		clear_global id;
 		introf;
@@ -167,21 +167,21 @@ let forall_tac backtrack continue seq=
        (tclORELSE
 	  (tclTHEN introf (tclCOMPLETE (wrap 0 true continue seq)))
 	  backtrack))
-    (if !qflag then 
+    (if !qflag then
        tclFAIL 0 (Pp.str "reversible in 1st order mode")
      else
        backtrack)
 
 let left_exists_tac ind backtrack id continue seq gls=
-  let n=(construct_nhyps ind gls).(0) in  
+  let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
       (simplest_elim (constr_of_global id))
       (tclTHENLIST [clear_global id;
                     tclDO n intro;
-                    (wrap (n-1) false continue seq)]) 
-      backtrack 
+                    (wrap (n-1) false continue seq)])
+      backtrack
       gls
-	
+
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
     (tclTHENS (cut prod)
@@ -190,7 +190,7 @@ let ll_forall_tac prod backtrack id continue seq=
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
 	      let term=mkApp((constr_of_global id),[|mkVar(id0)|]) in
-		tclTHEN (generalize [term]) (clear [id0]) gls);  
+		tclTHEN (generalize [term]) (clear [id0]) gls);
 	   clear_global id;
 	   intro;
 	   tclCOMPLETE (wrap 1 false continue (deepen seq))];
@@ -209,7 +209,7 @@ let defined_connectives=lazy
 
 let normalize_evaluables=
   onAllHypsAndConcl
-    (function 
+    (function
 	 None->unfold_in_concl (Lazy.force defined_connectives)
-       | Some id -> 
+       | Some id ->
 	   unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index b804c93ae..fc32621ca 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -49,6 +49,6 @@ val forall_tac : seqtac with_backtracking
 
 val left_exists_tac : inductive -> lseqtac with_backtracking
 
-val ll_forall_tac : types -> lseqtac with_backtracking 
+val ll_forall_tac : types -> lseqtac with_backtracking
 
 val normalize_evaluables : tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 98b178bde..685d44a84 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -27,7 +27,7 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 	begin
 	  match rf with
 	      Rarrow               -> 100
-	    | Rand                 ->  40 
+	    | Rand                 ->  40
 	    | Ror                  -> -15
 	    | Rfalse               -> -50
 	    | Rforall              -> 100
@@ -38,7 +38,7 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 	    Lfalse                 -> 999
 	  | Land _                 ->  90
 	  | Lor _                  ->  40
-	  | Lforall (_,_,_)        -> -30 
+	  | Lforall (_,_,_)        -> -30
 	  | Lexists _              ->  60
 	  | LA(_,lap) ->
 	      match lap with
@@ -48,7 +48,7 @@ let priority = (* pure heuristics, <=0 for non reversible *)
 		| LLor (_,_)       ->  70
 		| LLforall _       -> -20
 		| LLexists (_,_)   ->  50
-		| LLarrow  (_,_,_) -> -10 
+		| LLarrow  (_,_,_) -> -10
 
 let left_reversible lpat=(priority lpat)>0
 
@@ -71,15 +71,15 @@ let rec compare_list f l1 l2=
     | _,[] -> 1
     | (h1::q1),(h2::q2) -> (f =? (compare_list f)) h1 h2 q1 q2
 
-let compare_array f v1 v2=  
+let compare_array f v1 v2=
   let l=Array.length v1 in
   let c=l - Array.length v2 in
     if c=0 then
       let rec comp_aux i=
-	if i<0 then 0 
+	if i<0 then 0
 	else
 	  let ci=f v1.(i) v2.(i) in
-	    if ci=0 then 
+	    if ci=0 then
 	      comp_aux (i-1)
 	    else ci
       in comp_aux (l-1)
@@ -93,16 +93,16 @@ let compare_constr_int f t1 t2 =
     | Sort s1, Sort s2 -> Pervasives.compare s1 s2
     | Cast (c1,_,_), _ -> f c1 t2
     | _, Cast (c2,_,_) -> f t1 c2
-    | Prod (_,t1,c1), Prod (_,t2,c2) 
+    | Prod (_,t1,c1), Prod (_,t2,c2)
     | Lambda (_,t1,c1), Lambda (_,t2,c2) ->
-	(f =? f) t1 t2 c1 c2 
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
+	(f =? f) t1 t2 c1 c2
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
 	((f =? f) ==? f) b1 b2 t1 t2 c1 c2
     | App (_,_), App (_,_) ->
-	let c1,l1=decompose_app t1 
+	let c1,l1=decompose_app t1
 	and c2,l2=decompose_app t2 in
 	  (f =? (compare_list f)) c1 c2 l1 l2
-    | Evar (e1,l1), Evar (e2,l2) -> 
+    | Evar (e1,l1), Evar (e2,l2) ->
 	((-) =? (compare_array f)) e1 e2 l1 l2
     | Const c1, Const c2 -> Pervasives.compare c1 c2
     | Ind c1, Ind c2 -> Pervasives.compare c1 c2
@@ -119,7 +119,7 @@ let compare_constr_int f t1 t2 =
 
 let rec compare_constr m n=
   compare_constr_int compare_constr m n
-    
+
 module OrderedConstr=
 struct
   type t=constr
@@ -129,13 +129,13 @@ end
 type h_item = global_reference * (int*constr) option
 
 module Hitem=
-struct 
+struct
   type t = h_item
   let compare (id1,co1) (id2,co2)=
-    (Pervasives.compare 
+    (Pervasives.compare
      =? (fun oc1 oc2 ->
-	   match oc1,oc2 with 
-	       Some (m1,c1),Some (m2,c2) -> 
+	   match oc1,oc2 with
+	       Some (m1,c1),Some (m2,c2) ->
 		 ((-) =? OrderedConstr.compare) m1 m2 c1 c2
 	     | _,_->Pervasives.compare oc1 oc2)) id1 id2 co1 co2
 end
@@ -145,16 +145,16 @@ module CM=Map.Make(OrderedConstr)
 module History=Set.Make(Hitem)
 
 let cm_add typ nam cm=
-  try 
+  try
     let l=CM.find typ cm in CM.add typ (nam::l) cm
   with
       Not_found->CM.add typ [nam] cm
-	
+
 let cm_remove typ nam cm=
   try
-    let l=CM.find typ cm in 
+    let l=CM.find typ cm in
     let l0=List.filter (fun id->id<>nam) l in
-      match l0 with 
+      match l0 with
 	  []->CM.remove typ cm
 	| _ ->CM.add typ l0 cm
       with Not_found ->cm
@@ -172,7 +172,7 @@ type t=
      depth:int}
 
 let deepen seq={seq with depth=seq.depth-1}
- 
+
 let record item seq={seq with history=History.add item seq.history}
 
 let lookup item seq=
@@ -192,12 +192,12 @@ let rec add_formula side nam t seq gl=
 	begin
 	  match side with
 	      Concl ->
-		{seq with 
+		{seq with
 		   redexes=HP.add f seq.redexes;
 		   gl=f.constr;
 		   glatom=None}
 	    | _ ->
-		{seq with 
+		{seq with
 		   redexes=HP.add f seq.redexes;
 		   context=cm_add f.constr nam seq.context}
 	end
@@ -206,15 +206,15 @@ let rec add_formula side nam t seq gl=
 	    Concl ->
 	      {seq with gl=t;glatom=Some t}
 	  | _ ->
-	      {seq with 
+	      {seq with
 		 context=cm_add t nam seq.context;
 		 latoms=t::seq.latoms}
-	      
+
 let re_add_formula_list lf seq=
   let do_one f cm=
     if f.id == dummy_id then cm
     else cm_add f.constr f.id cm in
-  {seq with 
+  {seq with
      redexes=List.fold_right HP.add lf seq.redexes;
      context=List.fold_right do_one lf seq.context}
 
@@ -234,17 +234,17 @@ let rec take_formula 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 
+	if seq.gl==hd.constr then
 	  hd,nseq
 	else
 	  take_formula nseq (* discarding deprecated goal *)
     else
-      hd,{seq with 
+      hd,{seq with
 	    redexes=hp;
 	    context=cm_remove hd.constr hd.id seq.context}
-	
+
 let empty_seq depth=
-  {redexes=HP.empty;   
+  {redexes=HP.empty;
    context=CM.empty;
    latoms=[];
    gl=(mkMeta 1);
@@ -264,7 +264,7 @@ let expand_constructor_hints =
 let extend_with_ref_list l seq gl=
   let l = expand_constructor_hints l in
   let f gr seq=
-    let c=constr_of_global gr in    
+    let c=constr_of_global gr in
     let typ=(pf_type_of gl c) in
       add_formula Hyp gr typ seq gl in
     List.fold_right f l seq
@@ -277,8 +277,8 @@ let extend_with_auto_hints l seq gl=
     match p_a_t.code with
 	Res_pf (c,_) | Give_exact c
       | Res_pf_THEN_trivial_fail (c,_) ->
-	  (try 
-	     let gr=global_of_constr c in 
+	  (try
+	     let gr=global_of_constr c in
 	     let typ=(pf_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
@@ -288,7 +288,7 @@ let extend_with_auto_hints l seq gl=
     let hdb=
       try
 	searchtable_map dbname
-      with Not_found-> 
+      with Not_found->
 	error ("Firstorder: "^dbname^" : No such Hint database") in
       Hint_db.iter g hdb in
     List.iter h l;
@@ -297,16 +297,16 @@ let extend_with_auto_hints l seq gl=
 let print_cmap map=
   let print_entry c l s=
     let xc=Constrextern.extern_constr false (Global.env ()) c in
-      str "| " ++ 
-      Util.prlist Printer.pr_global l ++ 
+      str "| " ++
+      Util.prlist Printer.pr_global l ++
       str " : " ++
-      Ppconstr.pr_constr_expr xc ++ 
-      cut () ++ 
+      Ppconstr.pr_constr_expr xc ++
+      cut () ++
       s in
-    msgnl (v 0 
-	     (str "-----" ++ 
+    msgnl (v 0
+	     (str "-----" ++
 	      cut () ++
 	      CM.fold print_entry map (mt ()) ++
 	      str "-----"))
 
-	
+
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 206de27ed..ce0eddccc 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -46,7 +46,7 @@ val record: h_item -> t -> t
 
 val lookup: h_item -> t -> bool
 
-val add_formula : side -> global_reference -> constr -> t -> 
+val add_formula : side -> global_reference -> constr -> t ->
   Proof_type.goal sigma -> t
 
 val re_add_formula_list : Formula.t list -> t -> t
@@ -60,7 +60,7 @@ val empty_seq : int -> t
 val extend_with_ref_list : global_reference list ->
   t -> Proof_type.goal sigma -> t
 
-val extend_with_auto_hints : Auto.hint_db_name list -> 
+val extend_with_auto_hints : Auto.hint_db_name list ->
   t -> Proof_type.goal sigma -> t
 
-val print_cmap: global_reference list CM.t -> unit 
+val print_cmap: global_reference list CM.t -> unit
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 782129e5c..e3a4c6a55 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 open Util
-open Formula 
+open Formula
 open Tacmach
 open Term
 open Names
@@ -18,73 +18,73 @@ open Reductionops
 
 exception UFAIL of constr*constr
 
-(* 
-   RIGID-only Martelli-Montanari style unification for CLOSED terms 
-   I repeat : t1 and t2 must NOT have ANY free deBruijn                        
-   sigma is kept normal with respect to itself but is lazily applied 
-   to the equation set. Raises UFAIL with a pair of  terms 
+(*
+   RIGID-only Martelli-Montanari style unification for CLOSED terms
+   I repeat : t1 and t2 must NOT have ANY free deBruijn
+   sigma is kept normal with respect to itself but is lazily applied
+   to the equation set. Raises UFAIL with a pair of  terms
 *)
 
-let unif t1 t2= 
-  let bige=Queue.create () 
+let unif t1 t2=
+  let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
     sigma:=(i,t)::
       (List.map (function (n,tn)->(n,subst_meta [i,t] tn)) !sigma) in
-  let rec head_reduce t= 
+  let rec head_reduce t=
     (* forbids non-sigma-normal meta in head position*)
     match kind_of_term t with
 	Meta i->
-	  (try 
-	     head_reduce (List.assoc i !sigma) 
+	  (try
+	     head_reduce (List.assoc i !sigma)
 	   with Not_found->t)
-      | _->t in 
+      | _->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.empty t1) 
+      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
       and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
-	    Meta i,Meta j-> 
-	      if i<>j then 
+	    Meta i,Meta j->
+	      if i<>j then
 		if i<j then bind j nt1
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Intset.is_empty (free_rels t) && 
+		if Intset.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
-	  | _,Meta i -> 
+	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Intset.is_empty (free_rels t) && 
+		if Intset.is_empty (free_rels t) &&
 		  not (occur_term (mkMeta i) t) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
- 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige 
+ 	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast 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
-		if l<>(Array.length vb) then 
+		if l<>(Array.length vb) then
 		  raise (UFAIL (nt1,nt2))
-		else 
+		else
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
-		  done	  
+		  done
 	  | App(ha,va),App(hb,vb)->
 	      Queue.add (ha,hb) bige;
 	      let l=Array.length va in
-		if l<>(Array.length vb) then 
+		if l<>(Array.length vb) then
 		  raise (UFAIL (nt1,nt2))
-		else 
+		else
 		  for i=0 to l-1 do
 		    Queue.add (va.(i),vb.(i)) bige
 		  done
 	  | _->if not (eq_constr nt1 nt2) then raise (UFAIL (nt1,nt2))
     done;
-      assert false 
+      assert false
 	(* this place is unreachable but needed for the sake of typing *)
     with Queue.Empty-> !sigma
 
@@ -93,23 +93,23 @@ let value i t=
     if x<0 then y else if y<0 then x else x+y in
   let tref=mkMeta i in
   let rec vaux term=
-    if term=tref then 0 else 
+    if term=tref then 0 else
       let f v t=add v (vaux t) in
       let vr=fold_constr f (-1) term in
 	if vr<0 then -1 else vr+1 in
     vaux t
-	  
+
 type instance=
-    Real of (int*constr)*int 
-  | Phantom of constr 
+    Real of (int*constr)*int
+  | Phantom of constr
 
 let mk_rel_inst t=
   let new_rel=ref 1 in
   let rel_env=ref [] in
   let rec renum_rec d t=
-    match kind_of_term t with 
+    match kind_of_term t with
 	Meta n->
-	  (try 
+	  (try
 	     mkRel (d+(List.assoc n !rel_env))
 	   with Not_found->
 	     let m= !new_rel in
@@ -117,18 +117,18 @@ let mk_rel_inst t=
 	       rel_env:=(n,m) :: !rel_env;
 	       mkRel (m+d))
       | _ -> map_constr_with_binders succ renum_rec d t
-  in 
+  in
   let nt=renum_rec 0 t in (!new_rel - 1,nt)
 
 let unif_atoms i dom t1 t2=
-  try 
-    let t=List.assoc i (unif t1 t2) in 
+  try
+    let t=List.assoc i (unif t1 t2) in
       if isMeta t then Some (Phantom dom)
       else Some (Real(mk_rel_inst t,value i t1))
   with
       UFAIL(_,_) ->None
     | Not_found ->Some (Phantom dom)
-	   	  
+
 let renum_metas_from k n t= (* requires n = max (free_rels t) *)
   let l=list_tabulate (fun i->mkMeta (k+i)) n in
     substl l t
@@ -136,7 +136,7 @@ let renum_metas_from k n t= (* requires n = max (free_rels t) *)
 let more_general (m1,t1) (m2,t2)=
   let mt1=renum_metas_from 0 m1 t1
   and mt2=renum_metas_from m1 m2 t2 in
-    try 
+    try
       let sigma=unif mt1 mt2 in
       let p (n,t)= n<m1 || isMeta t in
 	List.for_all p sigma