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

1 files changed, 36 insertions, 36 deletions

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