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

diff --git a/checker/closure.ml b/checker/closure.ml
index 591b353db..b55c5848e 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -38,7 +38,7 @@ let incr_cnt red cnt =
   if red then begin
     if !stats then incr cnt;
     true
-  end else 
+  end else
     false
 
 let with_stats c =
@@ -127,13 +127,13 @@ module RedFlags = (struct
 	{ red with r_const = Idpred.remove id l1, l2 }
 
   let red_add_transparent red tr =
-    { red with r_const = tr } 
+    { red with r_const = tr }
 
   let mkflags = List.fold_left red_add no_red
 
   let red_set red = function
     | BETA -> incr_cnt red.r_beta beta
-    | CONST kn -> 
+    | CONST kn ->
 	let (_,l) = red.r_const in
 	let c = Cpred.mem kn l in
 	incr_cnt c delta
@@ -165,7 +165,7 @@ let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA]
 let betaiota = mkflags [fBETA;fIOTA]
 let beta = mkflags [fBETA]
 let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
-let unfold_red kn = 
+let unfold_red kn =
   let flag = match kn with
     | EvalVarRef id -> fVAR id
     | EvalConstRef kn -> fCONST kn
@@ -187,7 +187,7 @@ let betadeltaiota_red = {
   r_const = true,[],[];
   r_zeta = true;
   r_evar = true;
-  r_iota = true } 
+  r_iota = true }
 
 let betaiota_red = {
   r_beta = true;
@@ -195,7 +195,7 @@ let betaiota_red = {
   r_zeta = false;
   r_evar = false;
   r_iota = true }
-		     
+
 let beta_red = {
   r_beta = true;
   r_const = false,[],[];
@@ -231,7 +231,7 @@ let unfold_red kn =
 (* Sets of reduction kinds.
    Main rule: delta implies all consts (both global (= by
    kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
-   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
+   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
    a LetIn expression is Letin reduction *)
 
 type red_kind =
@@ -278,7 +278,7 @@ let red_local_const = red_delta_set
 (* to know if a redex is allowed, only a subset of red_kind is used ... *)
 let red_set red = function
   | BETA -> incr_cnt red.r_beta beta
-  | CONST [kn] -> 
+  | CONST [kn] ->
       let (b,l,_) = red.r_const in
       let c = List.mem kn l in
       incr_cnt ((b & not c) or (c & not b)) delta
@@ -339,7 +339,7 @@ type 'a infos = {
 let info_flags info = info.i_flags
 
 let ref_value_cache info ref =
-  try  
+  try
     Some (Hashtbl.find info.i_tab ref)
   with Not_found ->
   try
@@ -360,7 +360,7 @@ let ref_value_cache info ref =
 
 let defined_vars flags env =
 (*  if red_local_const (snd flags) then*)
-    fold_named_context 
+    fold_named_context
       (fun (id,b,_) e ->
 	 match b with
 	   | None -> e
@@ -370,7 +370,7 @@ let defined_vars flags env =
 
 let defined_rels flags env =
 (*  if red_local_const (snd flags) then*)
-  fold_rel_context 
+  fold_rel_context
       (fun (id,b,t) (i,subs) ->
 	 match b with
 	   | None -> (i+1, subs)
@@ -417,8 +417,8 @@ let neutr = function
   | (Whnf|Norm) -> Whnf
   | (Red|Cstr) -> Red
 
-type fconstr = { 
-  mutable norm: red_state; 
+type fconstr = {
+  mutable norm: red_state;
   mutable term: fterm }
 
 and fterm =
@@ -456,7 +456,7 @@ let update v1 (no,t) =
   else {norm=no;term=t}
 
 (**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *)
 
 type stack_member =
   | Zapp of fconstr array
@@ -504,7 +504,7 @@ let array_of_stack s =
   in Array.concat (stackrec s)
 let rec stack_assign s p c = match s with
   | Zapp args :: s ->
-      let q = Array.length args in 
+      let q = Array.length args in
       if p >= q then
 	Zapp args :: stack_assign s (p-q) c
       else
@@ -512,7 +512,7 @@ let rec stack_assign s p c = match s with
          nargs.(p) <- c;
          Zapp nargs :: s)
   | _ -> s
-let rec stack_tail p s = 
+let rec stack_tail p s =
   if p = 0 then s else
     match s with
       | Zapp args :: s ->
@@ -775,7 +775,7 @@ let term_of_fconstr =
 
 (* fstrong applies unfreeze_fun recursively on the (freeze) term and
  * yields a term.  Assumes that the unfreeze_fun never returns a
- * FCLOS term. 
+ * FCLOS term.
 let rec fstrong unfreeze_fun lfts v =
   to_constr (fstrong unfreeze_fun) lfts (unfreeze_fun v)
 *)
@@ -968,7 +968,7 @@ let rec knr info m stk =
   | FLambda(n,tys,f,e) when red_set info.i_flags fBETA ->
       (match get_args n tys f e stk with
           Inl e', s -> knit info e' f s
-        | Inr lam, s -> (lam,s)) 
+        | Inr lam, s -> (lam,s))
   | FFlex(ConstKey kn) when red_set info.i_flags (fCONST kn) ->
       (match ref_value_cache info (ConstKey kn) with
           Some v -> kni info v stk