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

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1bff68cbf0..bbc0ceae7d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -25,7 +25,7 @@ exception Elimconst
 
 
 (**********************************************************************)
-(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *) 
+(* The type of (machine) stacks (= lambda-bar-calculus' contexts)     *)
 
 type 'a stack_member =
   | Zapp of 'a list
@@ -80,12 +80,12 @@ let rec list_of_stack = function
 let rec app_stack = function
   | f, [] -> f
   | f, (Zapp [] :: s) -> app_stack (f, s)
-  | f, (Zapp args :: s) -> 
+  | f, (Zapp args :: s) ->
       app_stack (applist (f, args), s)
   | _ -> assert false
 let rec stack_assign s p c = match s with
   | Zapp args :: s ->
-      let q = List.length args in 
+      let q = List.length args in
       if p >= q then
 	Zapp args :: stack_assign s (p-q) c
       else
@@ -109,20 +109,20 @@ let rec stack_nth s p = match s with
   | _ -> raise Not_found
 
 (**************************************************************)
-(* The type of (machine) states (= lambda-bar-calculus' cuts) *) 
+(* The type of (machine) states (= lambda-bar-calculus' cuts) *)
 type state = constr * constr stack
 
 type  contextual_reduction_function = env ->  evar_map -> constr -> constr
 type  reduction_function =  contextual_reduction_function
 type local_reduction_function = evar_map -> constr -> constr
 
-type  contextual_stack_reduction_function = 
+type  contextual_stack_reduction_function =
     env ->  evar_map -> constr -> constr * constr list
 type  stack_reduction_function =  contextual_stack_reduction_function
 type local_stack_reduction_function =
     evar_map -> constr -> constr * constr list
 
-type  contextual_state_reduction_function = 
+type  contextual_state_reduction_function =
     env ->  evar_map -> state -> state
 type  state_reduction_function =  contextual_state_reduction_function
 type local_state_reduction_function = evar_map -> state -> state
@@ -159,16 +159,16 @@ let stack_reduction_of_reduction red_fun env sigma s =
   let t = red_fun env sigma (app_stack s) in
   whd_stack t
 
-let strong whdfun env sigma t = 
+let strong whdfun env sigma t =
   let rec strongrec env t =
     map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
   strongrec env t
 
-let local_strong whdfun sigma = 
+let local_strong whdfun sigma =
   let rec strongrec t = map_constr strongrec (whdfun sigma t) in
   strongrec
 
-let rec strong_prodspine redfun sigma c = 
+let rec strong_prodspine redfun sigma c =
   let x = redfun sigma c in
   match kind_of_term x with
     | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
@@ -203,7 +203,7 @@ module RedFlags = (struct
   type flags = int
   let fbeta = 1
   let fdelta = 2
-  let feta = 8 
+  let feta = 8
   let fiota = 16
   let fzeta = 32
   let mkflags = List.fold_left (lor) 0
@@ -282,7 +282,7 @@ let contract_fix ((recindices,bodynum),(types,names,bodies as typedbodies)) =
 let fix_recarg ((recindices,bodynum),_) stack =
   assert (0 <= bodynum & bodynum < Array.length recindices);
   let recargnum = Array.get recindices bodynum in
-  try 
+  try
     Some (recargnum, stack_nth stack recargnum)
   with Not_found ->
     None
@@ -303,12 +303,12 @@ let reduce_fix whdfun sigma fix stack =
 
 (* Y avait un commentaire pour whd_betadeltaiota :
 
-   NB : Cette fonction alloue peu c'est l'appel 
+   NB : Cette fonction alloue peu c'est l'appel
      ``let (c,cargs) = whfun (recarg, empty_stack)''
                               -------------------
    qui coute cher *)
 
-let rec whd_state_gen flags env sigma = 
+let rec whd_state_gen flags env sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | Rel n when red_delta flags ->
@@ -361,19 +361,19 @@ let rec whd_state_gen flags env sigma =
             whrec (reduce_mind_case
                      {mP=p; mconstr=c; mcargs=list_of_stack cargs;
 		      mci=ci; mlf=lf}, stack)
-          else 
+          else
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
-            
+
       | Fix fix when red_iota flags ->
 	  (match reduce_fix (fun _ -> whrec) sigma fix stack with
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
 
       | x -> s
-  in 
+  in
   whrec
 
-let local_whd_state_gen flags sigma = 
+let local_whd_state_gen flags sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
@@ -383,7 +383,7 @@ let local_whd_state_gen flags sigma =
           (match decomp_stack stack with
              | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
              | None when red_eta flags ->
-                 (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
+                 (match kind_of_term (app_stack (whrec (c, empty_stack))) with
                     | App (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
@@ -404,9 +404,9 @@ let local_whd_state_gen flags sigma =
             whrec (reduce_mind_case
                      {mP=p; mconstr=c; mcargs=list_of_stack cargs;
 		      mci=ci; mlf=lf}, stack)
-          else 
+          else
 	    (mkCase (ci, p, app_stack (c,cargs), lf), stack)
-            
+
       | Fix fix when red_iota flags ->
 	  (match reduce_fix (fun _ ->whrec) sigma fix stack with
              | Reduced s' -> whrec s'
@@ -423,7 +423,7 @@ let local_whd_state_gen flags sigma =
             | None -> s)
 
       | x -> s
-  in 
+  in
   whrec
 
 
@@ -464,7 +464,7 @@ let whd_betadelta env =
 let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
 let whd_betadeltaeta_stack env =
   stack_red_of_state_red (whd_betadeltaeta_state env)
-let whd_betadeltaeta env = 
+let whd_betadeltaeta env =
   red_of_state_red (whd_betadeltaeta_state env)
 
 (* 3. Iota reduction Functions *)
@@ -480,19 +480,19 @@ let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
 let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
 let whd_betadeltaiota_stack env =
   stack_red_of_state_red (whd_betadeltaiota_state env)
-let whd_betadeltaiota env = 
+let whd_betadeltaiota env =
   red_of_state_red (whd_betadeltaiota_state env)
 
 let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
 let whd_betadeltaiotaeta_stack env =
   stack_red_of_state_red (whd_betadeltaiotaeta_state env)
-let whd_betadeltaiotaeta env = 
+let whd_betadeltaiotaeta env =
   red_of_state_red (whd_betadeltaiotaeta_state env)
 
 let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
 let whd_betadeltaiota_nolet_stack env =
   stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
-let whd_betadeltaiota_nolet env = 
+let whd_betadeltaiota_nolet env =
   red_of_state_red (whd_betadeltaiota_nolet_state env)
 
 (* 3. Eta reduction Functions *)
@@ -530,53 +530,53 @@ let nf_betadeltaiota env sigma =
   clos_norm_flags Closure.betadeltaiota env sigma
 
 
-(* Attention reduire un beta-redexe avec un argument qui n'est pas 
+(* Attention reduire un beta-redexe avec un argument qui n'est pas
    une variable, peut changer enormement le temps de conversion lors
    du type checking :
      (fun x => x + x) M
 *)
-let rec whd_betaiota_preserving_vm_cast env sigma t = 	 
-   let rec stacklam_var subst t stack = 	 
-     match (decomp_stack stack,kind_of_term t) with 	 
-     | Some (h,stacktl), Lambda (_,_,c) -> 	 
-         begin match kind_of_term h with 	 
-         | Rel i when not (evaluable_rel i env) -> 	 
-             stacklam_var (h::subst) c stacktl 	 
-         | Var id when  not (evaluable_named id env)-> 	 
-             stacklam_var (h::subst) c stacktl 	 
-         | _ -> whrec (substl subst t, stack) 	 
-         end 	 
-     | _ -> whrec (substl subst t, stack) 	 
-   and whrec (x, stack as s) = 	 
-     match kind_of_term x with 	 
-       | Evar ev -> 	 
-           (match safe_evar_value sigma ev with 	 
-              | Some body -> whrec (body, stack) 	 
-              | None -> s) 	 
-       | Cast (c,VMcast,t) -> 	 
-           let c = app_stack (whrec (c,empty_stack)) in 	 
-           let t = app_stack (whrec (t,empty_stack)) in 	 
-           (mkCast(c,VMcast,t),stack) 	 
-       | Cast (c,DEFAULTcast,_) -> 	 
-           whrec (c, stack) 	 
-       | App (f,cl)  -> whrec (f, append_stack cl stack) 	 
-       | Lambda (na,t,c) -> 	 
-           (match decomp_stack stack with 	 
-            | Some (a,m) -> stacklam_var [a] c m 	 
-            | _ -> s) 	 
-       | Case (ci,p,d,lf) -> 	 
-           let (c,cargs) = whrec (d, empty_stack) in 	 
-           if reducible_mind_case c then 	 
-             whrec (reduce_mind_case 	 
-                      {mP=p; mconstr=c; mcargs=list_of_stack cargs; 	 
-                       mci=ci; mlf=lf}, stack) 	 
-           else 	 
-             (mkCase (ci, p, app_stack (c,cargs), lf), stack) 	 
-       | x -> s 	 
-   in 	 
+let rec whd_betaiota_preserving_vm_cast env sigma t =
+   let rec stacklam_var subst t stack =
+     match (decomp_stack stack,kind_of_term t) with
+     | Some (h,stacktl), Lambda (_,_,c) ->
+         begin match kind_of_term h with
+         | Rel i when not (evaluable_rel i env) ->
+             stacklam_var (h::subst) c stacktl
+         | Var id when  not (evaluable_named id env)->
+             stacklam_var (h::subst) c stacktl
+         | _ -> whrec (substl subst t, stack)
+         end
+     | _ -> whrec (substl subst t, stack)
+   and whrec (x, stack as s) =
+     match kind_of_term x with
+       | Evar ev ->
+           (match safe_evar_value sigma ev with
+              | Some body -> whrec (body, stack)
+              | None -> s)
+       | Cast (c,VMcast,t) ->
+           let c = app_stack (whrec (c,empty_stack)) in
+           let t = app_stack (whrec (t,empty_stack)) in
+           (mkCast(c,VMcast,t),stack)
+       | Cast (c,DEFAULTcast,_) ->
+           whrec (c, stack)
+       | App (f,cl)  -> whrec (f, append_stack cl stack)
+       | Lambda (na,t,c) ->
+           (match decomp_stack stack with
+            | Some (a,m) -> stacklam_var [a] c m
+            | _ -> s)
+       | Case (ci,p,d,lf) ->
+           let (c,cargs) = whrec (d, empty_stack) in
+           if reducible_mind_case c then
+             whrec (reduce_mind_case
+                      {mP=p; mconstr=c; mcargs=list_of_stack cargs;
+                       mci=ci; mlf=lf}, stack)
+           else
+             (mkCase (ci, p, app_stack (c,cargs), lf), stack)
+       | x -> s
+   in
    app_stack (whrec (t,empty_stack))
 
-let nf_betaiota_preserving_vm_cast = 
+let nf_betaiota_preserving_vm_cast =
   strong whd_betaiota_preserving_vm_cast
 
 (* lazy weak head reduction functions *)
@@ -638,12 +638,12 @@ let whd_meta metasubst c = match kind_of_term c with
 
 (* Try to replace all metas. Does not replace metas in the metas' values
  * Differs from (strong whd_meta). *)
-let plain_instance s c = 
+let plain_instance s c =
   let rec irec n u = match kind_of_term u with
     | Meta p -> (try lift n (List.assoc p s) with Not_found -> u)
     | App (f,l) when isCast f ->
         let (f,_,t) = destCast f in
-        let l' = Array.map (irec n) l in 
+        let l' = Array.map (irec n) l in
         (match kind_of_term f with
         | Meta p ->
 	    (* Don't flatten application nodes: this is used to extract a
@@ -651,21 +651,21 @@ let plain_instance s c =
                of the proof-tree *)
 	    (try let g = List.assoc p s in
 	    match kind_of_term g with
-            | App _ -> 
+            | App _ ->
                 let h = id_of_string "H" in
                 mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
-        | _ -> mkApp (irec n f,l'))	
+        | _ -> mkApp (irec n f,l'))
     | Cast (m,_,_) when isMeta m ->
 	(try lift n (List.assoc (destMeta m) s) with Not_found -> u)
     | _ ->
 	map_constr_with_binders succ irec n u
-  in 
+  in
   if s = [] then c else irec 0 c
 
 (* [instance] is used for [res_pf]; the call to [local_strong whd_betaiota]
-   has (unfortunately) different subtle side effects: 
+   has (unfortunately) different subtle side effects:
 
    - ** Order of subgoals **
      If the lemma is a case analysis with parameters, it will move the
@@ -682,7 +682,7 @@ let plain_instance s c =
      been contracted). A goal to rewrite may then fail or succeed
      differently.
 
-   - ** Naming of hypotheses ** 
+   - ** Naming of hypotheses **
      If a lemma is a function of the form "fun H:(forall a:A, P a)
      => .. F H .." where the expected type of H is "forall b:A, P b",
      then, without reduction, the application of the lemma will
@@ -713,24 +713,24 @@ let hnf_prod_app env sigma t n =
     | Prod (_,_,b) -> subst1 n b
     | _ -> anomaly "hnf_prod_app: Need a product"
 
-let hnf_prod_appvect env sigma t nl = 
+let hnf_prod_appvect env sigma t nl =
   Array.fold_left (hnf_prod_app env sigma) t nl
 
-let hnf_prod_applist env sigma t nl = 
+let hnf_prod_applist env sigma t nl =
   List.fold_left (hnf_prod_app env sigma) t nl
-				    
+
 let hnf_lam_app env sigma t n =
   match kind_of_term (whd_betadeltaiota env sigma t) with
     | Lambda (_,_,b) -> subst1 n b
     | _ -> anomaly "hnf_lam_app: Need an abstraction"
 
-let hnf_lam_appvect env sigma t nl = 
+let hnf_lam_appvect env sigma t nl =
   Array.fold_left (hnf_lam_app env sigma) t nl
 
-let hnf_lam_applist env sigma t nl = 
+let hnf_lam_applist env sigma t nl =
   List.fold_left (hnf_lam_app env sigma) t nl
 
-let splay_prod env sigma = 
+let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
@@ -738,10 +738,10 @@ let splay_prod env sigma =
 	  decrec (push_rel (n,None,a) env)
 	    ((n,a)::m) c0
       | _ -> m,t
-  in 
+  in
   decrec env []
 
-let splay_lam env sigma = 
+let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_betadeltaiota env sigma c in
     match kind_of_term t with
@@ -749,10 +749,10 @@ let splay_lam env sigma =
 	  decrec (push_rel (n,None,a) env)
 	    ((n,a)::m) c0
       | _ -> m,t
-  in 
+  in
   decrec env []
 
-let splay_prod_assum env sigma = 
+let splay_prod_assum env sigma =
   let rec prodec_rec env l c =
     let t = whd_betadeltaiota_nolet env sigma c in
     match kind_of_term t with
@@ -775,24 +775,24 @@ let splay_arity env sigma c =
 
 let sort_of_arity env c = snd (splay_arity env Evd.empty c)
 
-let splay_prod_n env sigma n = 
-  let rec decrec env m ln c = if m = 0 then (ln,c) else 
+let splay_prod_n env sigma n =
+  let rec decrec env m ln c = if m = 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
 	    (m-1) (add_rel_decl (n,None,a) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
-  in 
+  in
   decrec env n empty_rel_context
 
-let splay_lam_n env sigma n = 
-  let rec decrec env m ln c = if m = 0 then (ln,c) else 
+let splay_lam_n env sigma n =
+  let rec decrec env m ln c = if m = 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
 	    (m-1) (add_rel_decl (n,None,a) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
-  in 
+  in
   decrec env n empty_rel_context
 
 exception NotASort
@@ -803,22 +803,22 @@ let decomp_sort env sigma t =
   | _ -> raise NotASort
 
 let is_sort env sigma arity =
-  try let _ = decomp_sort env sigma arity in true 
+  try let _ = decomp_sort env sigma arity in true
   with NotASort -> false
 
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
 
 let whd_betaiota_deltazeta_for_iota_state env sigma s =
-  let rec whrec s = 
+  let rec whrec s =
     let (t, stack as s) = whd_betaiota_state sigma s in
     match kind_of_term t with
     | Case (ci,p,d,lf) ->
         let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
         let rslt = mkCase (ci, p, applist (cr,crargs), lf) in
-        if reducible_mind_case cr then 
+        if reducible_mind_case cr then
 	  whrec (rslt, stack)
-        else 
+        else
 	  s
     | Fix fix ->
 	  (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
@@ -832,15 +832,15 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s =
  * Used in Correctness.
  * Added by JCF, 29/1/98. *)
 
-let whd_programs_stack env sigma = 
+let whd_programs_stack env sigma =
   let rec whrec (x, stack as s) =
     match kind_of_term x with
       | App (f,cl) ->
 	  let n = Array.length cl - 1 in
 	  let c = cl.(n) in
-	  if occur_existential c then 
-	    s 
-	  else 
+	  if occur_existential c then
+	    s
+	  else
 	    whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack)
       | LetIn (_,b,_,c) ->
 	  if occur_existential b then
@@ -867,7 +867,7 @@ let whd_programs_stack env sigma =
              | Reduced s' -> whrec s'
 	     | NotReducible -> s)
       | _ -> s
-  in 
+  in
   whrec
 
 let whd_programs env sigma x =
@@ -882,7 +882,7 @@ let find_conclusion env sigma =
       | Prod (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
       | Lambda (x,t,c0) -> decrec (push_rel (x,None,t) env) c0
       | t -> t
-  in 
+  in
   decrec env
 
 let is_arity env sigma c =
@@ -893,29 +893,29 @@ let is_arity env sigma c =
 (*************************************)
 (* Metas *)
 
-let meta_value evd mv = 
+let meta_value evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
-    | Some (b,_) -> 
+    | Some (b,_) ->
       instance
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
     | None -> mkMeta mv
-  in 
+  in
   valrec mv
 
 let meta_instance env b =
   let c_sigma =
-    List.map 
+    List.map
       (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas)
-  in 
+  in
   if c_sigma = [] then b.rebus else instance c_sigma b.rebus
 
 let nf_meta env c = meta_instance env (mk_freelisted c)
 
 (* Instantiate metas that create beta/iota redexes *)
 
-let meta_value evd mv = 
+let meta_value evd mv =
   let rec valrec mv =
     match meta_opt_fvalue evd mv with
     | Some (b,_) ->
@@ -923,14 +923,14 @@ let meta_value evd mv =
         (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas))
         b.rebus
     | None -> mkMeta mv
-  in 
+  in
   valrec mv
 
 let meta_reducible_instance evd b =
   let fm = Metaset.elements b.freemetas in
-  let metas = List.fold_left (fun l mv -> 
+  let metas = List.fold_left (fun l mv ->
     match (try meta_opt_fvalue evd mv with Not_found -> None) with
-    | Some (g,(_,s)) -> (mv,(g.rebus,s))::l 
+    | Some (g,(_,s)) -> (mv,(g.rebus,s))::l
     | None -> l) [] fm in
   let rec irec u =
     let u = whd_betaiota Evd.empty u in
@@ -959,21 +959,21 @@ let meta_reducible_instance evd b =
 	(try let g,s = List.assoc m metas in if s<>CoerceToType then irec g else u
 	 with Not_found -> u)
     | _ -> map_constr irec u
-  in 
+  in
   if fm = [] then (* nf_betaiota? *) b.rebus else irec b.rebus
 
 
-let head_unfold_under_prod ts env _ c = 
-  let unfold cst = 
+let head_unfold_under_prod ts env _ c =
+  let unfold cst =
     if Cpred.mem cst (snd ts) then
       match constant_opt_value env cst with
-	| Some c -> c 
+	| Some c -> c
 	| None -> mkConst cst
     else mkConst cst in
   let rec aux c =
     match kind_of_term c with
       | Prod (n,t,c) -> mkProd (n,aux t, aux c)
-      | _ -> 
+      | _ ->
 	  let (h,l) = decompose_app c in
 	  match kind_of_term h with
 	    | Const cst -> beta_applist (unfold cst,l)