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, 25 insertions, 25 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 89f1b443b9..0a404fff31 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -22,7 +22,7 @@ let unfold_reference ((ids, csts), infos) k =
     | VarKey id when not (Idpred.mem id ids) -> None
     | ConstKey cst when not (Cpred.mem cst csts) -> None
     | _ -> unfold_reference infos k
-	  
+
 let rec is_empty_stack = function
     [] -> true
   | Zupdate _::s -> is_empty_stack s
@@ -96,13 +96,13 @@ let whd_betaiotazeta x =
        Prod _|Lambda _|Fix _|CoFix _) -> x
     | _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
 
-let whd_betadeltaiota env t = 
+let whd_betadeltaiota env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _) -> t
     | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
 
-let whd_betadeltaiota_nolet env t = 
+let whd_betadeltaiota_nolet env t =
   match kind_of_term t with
     | (Sort _|Meta _|Evar _|Ind _|Construct _|
        Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
@@ -167,8 +167,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
     and this holds whatever Set is predicative or impredicative
 *)
 
-type conv_pb = 
-  | CONV 
+type conv_pb =
+  | CONV
   | CUMUL
 
 let sort_cmp pb s0 s1 cuniv =
@@ -227,7 +227,7 @@ let in_whnf (t,stk) =
     | FLOCKED -> assert false
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
+let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv =
   eqappr cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
@@ -249,7 +249,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
     (* case of leaves *)
     | (FAtom a1, FAtom a2) ->
 	(match kind_of_term a1, kind_of_term a2 with
-	   | (Sort s1, Sort s2) -> 
+	   | (Sort s1, Sort s2) ->
 	       assert (is_empty_stack v1 && is_empty_stack v2);
 	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
@@ -299,7 +299,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, _)      ->
         (match unfold_reference infos fl1 with
-           | Some def1 -> 
+           | Some def1 ->
 	       eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
            | None -> raise NotConvertible)
     | (_, FFlex fl2)      ->
@@ -307,7 +307,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
            | Some def2 ->
 	       eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
            | None -> raise NotConvertible)
-	
+
     (* other constructors *)
     | (FLambda _, FLambda _) ->
         assert (is_empty_stack v1 && is_empty_stack v2);
@@ -346,7 +346,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
            let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
 	   let u1 = convert_vect infos el1 el2 fty1 fty2 cuniv in
            let u2 =
-             convert_vect infos 
+             convert_vect infos
 		 (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 u1 in
            convert_stacks infos lft1 lft2 v1 v2 u2
          else raise NotConvertible
@@ -370,7 +370,7 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
      | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_)
        | (_, FLetIn _) | (_,FCases _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _)
        | (FLOCKED,_) | (_,FLOCKED) ) -> assert false
-    
+
      (* In all other cases, terms are not convertible *)
      | _ -> raise NotConvertible
 
@@ -384,8 +384,8 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
   if lv1 = lv2
-  then 
-    let rec fold n univ = 
+  then
+    let rec fold n univ =
       if n >= lv1 then univ
       else
         let u1 = ccnv CONV infos lft1 lft2 v1.(n) v2.(n) univ in
@@ -412,10 +412,10 @@ let conv ?(evars=fun _->None) = fconv CONV evars
 let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
 
 let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
-  array_fold_left2_i 
+  array_fold_left2_i
     (fun i c t1 t2 ->
       let c' =
-        try conv_leq ~evars env t1 t2 
+        try conv_leq ~evars env t1 t2
         with NotConvertible -> raise (NotConvertibleVect i) in
       Constraint.union c c')
     Constraint.empty
@@ -426,25 +426,25 @@ let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
 
 let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 let set_vm_conv f = vm_conv := f
-let vm_conv cv_pb env t1 t2 = 
-  try 
+let vm_conv cv_pb env t1 t2 =
+  try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
       fconv cv_pb (fun _->None) env t1 t2
-  
+
 
 let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
 
 let set_default_conv f = default_conv := f
 
-let default_conv cv_pb env t1 t2 = 
-  try 
+let default_conv cv_pb env t1 t2 =
+  try
     !default_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
       fconv cv_pb (fun _->None) env t1 t2
-  
+
 let default_conv_leq = default_conv CUMUL
 (*
 let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
@@ -471,12 +471,12 @@ let hnf_prod_app env t n =
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly "hnf_prod_app: Need a product"
 
-let hnf_prod_applist env t nl = 
+let hnf_prod_applist env t nl =
   List.fold_left (hnf_prod_app env) t nl
 
 (* Dealing with arities *)
 
-let dest_prod env = 
+let dest_prod env =
   let rec decrec env m c =
     let t = whd_betadeltaiota env c in
     match kind_of_term t with
@@ -484,11 +484,11 @@ let dest_prod env =
           let d = (n,None,a) in
 	  decrec (push_rel d env) (add_rel_decl d m) c0
       | _ -> m,t
-  in 
+  in
   decrec env empty_rel_context
 
 (* The same but preserving lets *)
-let dest_prod_assum env = 
+let dest_prod_assum env =
   let rec prodec_rec env l ty =
     let rty = whd_betadeltaiota_nolet env ty in
     match kind_of_term rty with