Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 115 insertions, 126 deletions

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 99ec1650..5bcba626 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *)
+(* $Id$ *)
 
 open Util
 open Names
@@ -55,7 +55,7 @@ let inductive_params (mib,_) = mib.mind_nparams
 (* inductives *)
 let ind_subst mind mib =
   let ntypes = mib.mind_ntypes in
-  let make_Ik k = mkInd (mind,ntypes-k-1) in 
+  let make_Ik k = mkInd (mind,ntypes-k-1) in
   list_tabulate make_Ik ntypes
 
 (* Instantiate inductives in constructor type *)
@@ -64,7 +64,7 @@ let constructor_instantiate mind mib c =
   substl s c
 
 let instantiate_params full t args sign =
-  let fail () = 
+  let fail () =
     anomaly "instantiate_params: type, ctxt and args mismatch" in
   let (rem_args, subs, ty) =
     Sign.fold_rel_context
@@ -75,7 +75,7 @@ let instantiate_params full t args sign =
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
       sign
-      ~init:(args,[],t) 
+      ~init:(args,[],t)
   in
   if rem_args <> [] then fail();
   substl subs ty
@@ -101,11 +101,11 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) =
 let number_of_inductives mib = Array.length mib.mind_packets
 let number_of_constructors mip = Array.length mip.mind_consnames
 
-(* 
+(*
 Computing the actual sort of an applied or partially applied inductive type:
 
 I_i: forall uniformparams:utyps, forall otherparams:otyps, Type(a)
-uniformargs : utyps 
+uniformargs : utyps
 otherargs : otyps
 I_1:forall ...,s_1;...I_n:forall ...,s_n |- sort(C_kj(uniformargs)) = s_kj
 s'_k = max(..s_kj..)
@@ -221,11 +221,11 @@ let type_of_constructor cstr (mib,mip) =
   if i > nconstr then error "Not enough constructors in the type.";
   constructor_instantiate (fst ind) mib specif.(i-1)
 
-let arities_of_specif kn (mib,mip) = 
+let arities_of_specif kn (mib,mip) =
   let specif = mip.mind_nf_lc in
   Array.map (constructor_instantiate kn mib) specif
 
-let arities_of_constructors ind specif = 
+let arities_of_constructors ind specif =
   arities_of_specif (fst ind) specif
 
 let type_of_constructors ind (mib,mip) =
@@ -250,7 +250,7 @@ let local_rels ctxt =
             None   -> (mkRel n :: rels, n+1)
           | Some _ -> (rels, n+1))
       ~init:([],1)
-      ctxt 
+      ctxt
   in
   rels
 
@@ -258,7 +258,7 @@ let local_rels ctxt =
 
 let inductive_sort_family mip =
   match mip.mind_arity with
-   | Monomorphic s -> family_of_sort s.mind_sort 
+   | Monomorphic s -> family_of_sort s.mind_sort
    | Polymorphic _ -> InType
 
 let mind_arity mip =
@@ -270,26 +270,30 @@ let get_instantiated_arity (mib,mip) params =
 
 let elim_sorts (_,mip) = mip.mind_kelim
 
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
-  in 
-  reln [] 1
+let extended_rel_list n hyps =
+  let rec reln l p = function
+    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
+    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
+    | [] -> l
+  in
+  reln [] 1 hyps
 
 let build_dependent_inductive ind (_,mip) params =
-  let nrealargs = mip.mind_nrealargs in
-  applist 
-    (mkInd ind, (List.map (lift nrealargs) params)@(rel_list 0 nrealargs))
+  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  applist
+    (mkInd ind,
+       List.map (lift mip.mind_nrealargs_ctxt) params
+       @ extended_rel_list 0 realargs)
 
 (* This exception is local *)
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
 
 let check_allowed_sort ksort specif =
-  if not (List.exists ((=) ksort) (elim_sorts specif)) then 
+  if not (List.exists ((=) ksort) (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
     raise (LocalArity (Some(ksort,s,error_elim_expln ksort s)))
 
-let is_correct_arity env c pj ind specif params = 
+let is_correct_arity env c pj ind specif params =
   let arsign,_ = get_instantiated_arity specif params in
   let rec srec env pt ar u =
     let pt' = whd_betadeltaiota env pt in
@@ -301,20 +305,19 @@ let is_correct_arity env c pj ind specif params =
           srec (push_rel (na1,None,a1) env) t ar' (Constraint.union u univ)
       | Prod (_,a1,a2), [] -> (* whnf of t was not needed here! *)
           let ksort = match kind_of_term (whd_betadeltaiota env a2) with
-            | Sort s -> family_of_sort s 
+            | Sort s -> family_of_sort s
 	    | _ -> raise (LocalArity None) in
-	  let dep_ind = build_dependent_inductive ind specif params in 
+	  let dep_ind = build_dependent_inductive ind specif params in
           let univ =
             try conv env a1 dep_ind
             with NotConvertible -> raise (LocalArity None) in
 	  check_allowed_sort ksort specif;
-	  (true, Constraint.union u univ)
-      | Sort s', [] ->
-	  check_allowed_sort (family_of_sort s') specif;
-	  (false, u)
+	  Constraint.union u univ
+      | _, (_,Some _,_ as d)::ar' ->
+	  srec (push_rel d env) (lift 1 pt') ar' u
       | _ ->
 	  raise (LocalArity None)
-  in 
+  in
   try srec env pj.uj_type (List.rev arsign) Constraint.empty
   with LocalArity kinds ->
     error_elim_arity env ind (elim_sorts specif) c pj kinds
@@ -325,7 +328,7 @@ let is_correct_arity env c pj ind specif params =
 
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
    and [cty] is the type of the constructor (params not instantiated) *)
-let build_branches_type ind (_,mip as specif) params dep p =
+let build_branches_type ind (_,mip as specif) params p =
   let build_one_branch i cty =
     let typi = full_constructor_instantiate (ind,specif,params) cty in
     let (args,ccl) = decompose_prod_assum typi in
@@ -333,50 +336,36 @@ let build_branches_type ind (_,mip as specif) params dep p =
     let (_,allargs) = decompose_app ccl in
     let (lparams,vargs) = list_chop (inductive_params specif) allargs in
     let cargs =
-      if dep then
-        let cstr = ith_constructor_of_inductive ind (i+1) in
-        let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
-        vargs @ [dep_cstr]
-      else
-        vargs in
+      let cstr = ith_constructor_of_inductive ind (i+1) in
+      let dep_cstr = applist (mkConstruct cstr,lparams@(local_rels args)) in
+      vargs @ [dep_cstr] in
     let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base args in
   Array.mapi build_one_branch mip.mind_nf_lc
 
 (* [p] is the predicate, [c] is the match object, [realargs] is the
    list of real args of the inductive type *)
-let build_case_type dep p c realargs =
-  let args = if dep then realargs@[c] else realargs in
-  beta_appvect p (Array.of_list args)
+let build_case_type n p c realargs =
+  whd_betaiota (betazeta_appvect (n+1) p (Array.of_list (realargs@[c])))
 
 let type_case_branches env (ind,largs) pj c =
-  let specif = lookup_mind_specif env ind in 
+  let specif = lookup_mind_specif env ind in
   let nparams = inductive_params specif in
   let (params,realargs) = list_chop nparams largs in
   let p = pj.uj_val in
-  let (dep,univ) = is_correct_arity env c pj ind specif params in
-  let lc = build_branches_type ind specif params dep p in
-  let ty = build_case_type dep p c realargs in
+  let univ = is_correct_arity env c pj ind specif params in
+  let lc = build_branches_type ind specif params p in
+  let ty = build_case_type (snd specif).mind_nrealargs_ctxt p c realargs in
   (lc, ty, univ)
 
 
 (************************************************************************)
 (* Checking the case annotation is relevent *)
 
-let rec inductive_kn_equiv env kn1 kn2 =
-  match (lookup_mind kn1 env).mind_equiv with
-    | Some kn1' -> inductive_kn_equiv env kn2 kn1'
-    | None -> match (lookup_mind kn2 env).mind_equiv with
-        | Some kn2' -> inductive_kn_equiv env kn2' kn1
-	| None -> false
-
-let inductive_equiv env (kn1,i1) (kn2,i2) =
-  i1=i2 & inductive_kn_equiv env kn1 kn2
-
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (Closure.mind_equiv env indsp ci.ci_ind) or
+    not (eq_ind indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
     (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
@@ -386,7 +375,7 @@ let check_case_info env indsp ci =
 
 (* Guard conditions for fix and cofix-points *)
 
-(* Check if t is a subterm of Rel n, and gives its specification, 
+(* Check if t is a subterm of Rel n, and gives its specification,
    assuming lst already gives index of
    subterms with corresponding specifications of recursive arguments *)
 
@@ -431,7 +420,7 @@ type subterm_spec =
 
 let spec_of_tree t =
   if Rtree.eq_rtree (=) t mk_norec then Not_subterm else Subterm(Strict,t)
- 
+
 let subterm_spec_glb =
   let glb2 s1 s2 =
     match s1,s2 with
@@ -444,7 +433,7 @@ let subterm_spec_glb =
           (* branches do not return objects with same spec *)
           else Not_subterm in
   Array.fold_left glb2 Dead_code
-          
+
 type guard_env =
   { env     : env;
     (* dB of last fixpoint *)
@@ -468,7 +457,7 @@ let make_renv env minds recarg (kn,tyi) =
     genv = [Subterm(Large,mind_recvec.(tyi))] }
 
 let push_var renv (x,ty,spec) =
-  { renv with 
+  { renv with
     env = push_rel (x,None,ty) renv.env;
     rel_min = renv.rel_min+1;
     genv = spec:: renv.genv }
@@ -480,7 +469,7 @@ let push_var_renv renv (x,ty) =
   push_var renv (x,ty,Not_subterm)
 
 (* Fetch recursive information about a variable p *)
-let subterm_var p renv = 
+let subterm_var p renv =
   try List.nth renv.genv (p-1)
   with Failure _ | Invalid_argument _ -> Not_subterm
 
@@ -490,7 +479,7 @@ let add_subterm renv (x,a,spec) =
 
 let push_ctxt_renv renv ctxt =
   let n = rel_context_length ctxt in
-  { renv with 
+  { renv with
     env = push_rel_context ctxt renv.env;
     rel_min = renv.rel_min+n;
     genv = iterate (fun ge -> Not_subterm::ge) n renv.genv }
@@ -529,8 +518,8 @@ let lookup_subterms env ind =
    associated to its own subterms.
    Rq: if branch is not eta-long, then the recursive information
    is not propagated to the missing abstractions *)
-let case_branches_specif renv c_spec ind lbr = 
-  let rec push_branch_args renv lrec c = 
+let case_branches_specif renv c_spec ind lbr =
+  let rec push_branch_args renv lrec c =
     match lrec with
         ra::lr ->
           let c' = whd_betadeltaiota renv.env c in
@@ -546,7 +535,7 @@ let case_branches_specif renv c_spec ind lbr =
         let sub_spec = Array.map (List.map spec_of_tree) (dest_subterms t) in
         assert (Array.length sub_spec = Array.length lbr);
         array_map2 (push_branch_args renv) sub_spec lbr
-    | Dead_code -> 
+    | Dead_code ->
         let t = dest_subterms (lookup_subterms renv.env ind) in
         let sub_spec = Array.map (List.map (fun _ -> Dead_code)) t in
         assert (Array.length sub_spec = Array.length lbr);
@@ -559,22 +548,19 @@ let case_branches_specif renv c_spec ind lbr =
    about variables.
 *)
 
-let rec subterm_specif renv t = 
+let rec subterm_specif renv t =
   (* maybe reduction is not always necessary! *)
   let f,l = decompose_app (whd_betadeltaiota renv.env t) in
-  match kind_of_term f with 
+  match kind_of_term f with
     | Rel k -> subterm_var k renv
 
     | Case (ci,_,c,lbr) ->
-        if Array.length lbr = 0 then Dead_code
-        else
-          let c_spec = subterm_specif renv c in
-          let lbr_spec = case_branches_specif renv c_spec ci.ci_ind lbr in
-          let stl  =
-            Array.map (fun (renv',br') -> subterm_specif renv' br')
-              lbr_spec in
-          subterm_spec_glb stl
-	       
+        let lbr_spec = case_subterm_specif renv ci c lbr in
+        let stl  =
+          Array.map (fun (renv',br') -> subterm_specif renv' br')
+            lbr_spec in
+        subterm_spec_glb stl
+
     | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
 (* when proving that the fixpoint f(x)=e is less than n, it is enough
    to prove that e is less than n assuming f is less than n
@@ -597,7 +583,7 @@ let rec subterm_specif renv t =
                 (* Why Strict here ? To be general, it could also be
                    Large... *)
                 assign_var_spec renv' (nbfix-i, Subterm(Strict,recargs)) in
-              let decrArg = recindxs.(i) in 
+              let decrArg = recindxs.(i) in
               let theBody = bodies.(i)   in
               let nbOfAbst = decrArg+1 in
               let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in
@@ -611,7 +597,7 @@ let rec subterm_specif renv t =
                   assign_var_spec renv'' (1, arg_spec) in
 	      subterm_specif renv'' strippedBody)
 
-    | Lambda (x,a,b) -> 
+    | Lambda (x,a,b) ->
         assert (l=[]);
         subterm_specif (push_var_renv renv (x,a)) b
 
@@ -621,9 +607,14 @@ let rec subterm_specif renv t =
     (* Other terms are not subterms *)
     | _ -> Not_subterm
 
-
+and case_subterm_specif renv ci c lbr =
+  if Array.length lbr = 0 then [||]
+  else
+    let c_spec = subterm_specif renv c in
+    case_branches_specif renv c_spec ci.ci_ind lbr
+ 
 (* Check term c can be applied to one of the mutual fixpoints. *)
-let check_is_subterm renv c = 
+let check_is_subterm renv c =
   match subterm_specif renv c with
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
@@ -651,21 +642,21 @@ let error_partial_apply renv fx =
    given [recpos], the decreasing arguments of each mutually defined
    fixpoint. *)
 let check_one_fix renv recpos def =
-  let nfi = Array.length recpos in 
+  let nfi = Array.length recpos in
 
   (* Checks if [t] only make valid recursive calls *)
-  let rec check_rec_call renv t = 
+  let rec check_rec_call renv t =
     (* if [t] does not make recursive calls, it is guarded: *)
     if noccur_with_meta renv.rel_min nfi t then ()
     else
       let (f,l) = decompose_app (whd_betaiotazeta t) in
       match kind_of_term f with
-        | Rel p -> 
-            (* Test if [p] is a fixpoint (recursive call) *) 
+        | Rel p ->
+            (* Test if [p] is a fixpoint (recursive call) *)
 	    if renv.rel_min <= p & p < renv.rel_min+nfi then
               begin
                 List.iter (check_rec_call renv) l;
-                (* the position of the invoked fixpoint: *) 
+                (* the position of the invoked fixpoint: *)
 	        let glob = renv.rel_min+nfi-1-p in
                 (* the decreasing arg of the rec call: *)
 	        let np = recpos.(glob) in
@@ -691,31 +682,29 @@ let check_one_fix renv recpos def =
             List.iter (check_rec_call renv) (c_0::p::l);
             (* compute the recarg information for the arguments of
                each branch *)
-            let c_spec = subterm_specif renv c_0 in
-            let lbr = case_branches_specif renv c_spec ci.ci_ind lrest in
+            let lbr = case_subterm_specif renv ci c_0 lrest in
             Array.iter (fun (renv',br') -> check_rec_call renv' br') lbr
 
         (* Enables to traverse Fixpoint definitions in a more intelligent
            way, ie, the rule :
-           if - g = Fix g/p := [y1:T1]...[yp:Tp]e &
-              - f is guarded with respect to the set of pattern variables S 
+           if - g = fix g (y1:T1)...(yp:Tp) {struct yp} := e &
+              - f is guarded with respect to the set of pattern variables S
                 in a1 ... am        &
-              - f is guarded with respect to the set of pattern variables S 
+              - f is guarded with respect to the set of pattern variables S
                 in T1 ... Tp        &
               - ap is a sub-term of the formal argument of f &
               - f is guarded with respect to the set of pattern variables
                 S+{yp} in e
            then f is guarded with respect to S in (g a1 ... am).
            Eduardo 7/9/98 *)
-
         | Fix ((recindxs,i),(_,typarray,bodies as recdef)) ->
             List.iter (check_rec_call renv) l;
             Array.iter (check_rec_call renv) typarray;
             let decrArg = recindxs.(i) in
-            let renv' = push_fix_renv renv recdef in 
+            let renv' = push_fix_renv renv recdef in
             if (List.length l < (decrArg+1)) then
 	      Array.iter (check_rec_call renv') bodies
-            else 
+            else
               Array.iteri
                 (fun j body ->
                   if i=j then
@@ -725,8 +714,8 @@ let check_one_fix renv recpos def =
                   else check_rec_call renv' body)
                 bodies
 
-        | Const kn -> 
-            if evaluable_constant kn renv.env then 
+        | Const kn ->
+            if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv) l
               with (FixGuardError _ ) ->
 	        check_rec_call renv(applist(constant_value renv.env kn, l))
@@ -734,14 +723,14 @@ let check_one_fix renv recpos def =
 
         (* The cases below simply check recursively the condition on the
            subterms *)
-        | Cast (a,_, b) -> 
+        | Cast (a,_, b) ->
             List.iter (check_rec_call renv) (a::b::l)
 
         | Lambda (x,a,b) ->
             List.iter (check_rec_call renv) (a::l);
             check_rec_call (push_var_renv renv (x,a)) b
 
-        | Prod (x,a,b) -> 
+        | Prod (x,a,b) ->
             List.iter (check_rec_call renv) (a::l);
             check_rec_call (push_var_renv renv (x,a)) b
 
@@ -787,9 +776,9 @@ let judgment_of_fixpoint (_, types, bodies) =
   array_map2 (fun typ body -> { uj_val = body ; uj_type = typ }) types bodies
 
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
-  let nbfix = Array.length bodies in 
+  let nbfix = Array.length bodies in
   if nbfix = 0
-    or Array.length nvect <> nbfix 
+    or Array.length nvect <> nbfix
     or Array.length types <> nbfix
     or Array.length names <> nbfix
     or bodynum < 0
@@ -800,18 +789,18 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let raise_err env i err =
     error_ill_formed_rec_body env err names i fixenv vdefj in
   (* Check the i-th definition with recarg k *)
-  let find_ind i k def = 
-    (* check fi does not appear in the k+1 first abstractions, 
+  let find_ind i k def =
+    (* check fi does not appear in the k+1 first abstractions,
        gives the type of the k+1-eme abstraction (must be an inductive)  *)
-    let rec check_occur env n def = 
+    let rec check_occur env n def =
       match kind_of_term (whd_betadeltaiota env def) with
-        | Lambda (x,a,b) -> 
+        | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (x, None, a) env in
               if n = k+1 then
                 (* get the inductive type of the fixpoint *)
-                let (mind, _) = 
-                  try find_inductive env a 
+                let (mind, _) =
+                  try find_inductive env a
                   with Not_found ->
 		    raise_err env i (RecursionNotOnInductiveType a) in
                 (mind, (env', b))
@@ -831,7 +820,7 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
     let renv = make_renv fenv minds nvect.(i) minds.(i) in
     try check_one_fix renv nvect body
     with FixGuardError (fixenv,err) ->
-      error_ill_formed_rec_body fixenv err names i 
+      error_ill_formed_rec_body fixenv err names i
 	(push_rec_types recdef env) (judgment_of_fixpoint recdef)
   done
 
@@ -852,17 +841,17 @@ let rec codomain_is_coind env c =
   let b = whd_betadeltaiota env c in
   match kind_of_term b with
     | Prod (x,a,b) ->
-	codomain_is_coind (push_rel (x, None, a) env) b 
-    | _ -> 
+	codomain_is_coind (push_rel (x, None, a) env) b
+    | _ ->
 	(try find_coinductive env b
         with Not_found ->
 	  raise (CoFixGuardError (env, CodomainNotInductiveType b)))
 
-let check_one_cofix env nbfix def deftype = 
+let check_one_cofix env nbfix def deftype =
   let rec check_rec_call env alreadygrd n vlra  t =
     if not (noccur_with_meta n nbfix t) then
       let c,args = decompose_app (whd_betadeltaiota env t) in
-      match kind_of_term c with 
+      match kind_of_term c with
 	| Rel p when  n <= p && p < n+nbfix ->
 	    (* recursive call: must be guarded and no nested recursive
                call allowed *)
@@ -870,14 +859,14 @@ let check_one_cofix env nbfix def deftype =
 	      raise (CoFixGuardError (env,UnguardedRecursiveCall t))
             else if not(List.for_all (noccur_with_meta n nbfix) args) then
 	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
-		 
+
 	| Construct (_,i as cstr_kn)  ->
-            let lra = vlra.(i-1) in 
+            let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
 	    let (mib,mip) = lookup_mind_specif env mI in
             let realargs = list_skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
-              | (t::lr), (rar::lrar) -> 
+              | (t::lr), (rar::lrar) ->
                   if rar = mk_norec then
                     if noccur_with_meta n nbfix t
                     then process_args_of_constr (lr, lrar)
@@ -888,26 +877,26 @@ let check_one_cofix env nbfix def deftype =
                     check_rec_call env true n spec t;
                     process_args_of_constr (lr, lrar)
               | [],_ -> ()
-              | _ -> anomaly_ill_typed () 
+              | _ -> anomaly_ill_typed ()
             in process_args_of_constr (realargs, lra)
-		 
+
 	| Lambda (x,a,b) ->
 	     assert (args = []);
             if noccur_with_meta n nbfix a then
               let env' = push_rel (x, None, a) env in
               check_rec_call env' alreadygrd (n+1)  vlra b
-            else 
+            else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
-	      
+
 	| CoFix (j,(_,varit,vdefs as recdef)) ->
             if (List.for_all (noccur_with_meta n nbfix) args)
-            then 
+            then
               let nbfix = Array.length vdefs in
 	      if (array_for_all (noccur_with_meta n nbfix) varit) then
 		let env' = push_rec_types recdef env in
 		(Array.iter (check_rec_call env' alreadygrd (n+1) vlra) vdefs;
 		 List.iter (check_rec_call env alreadygrd n vlra) args)
-              else 
+              else
 		raise (CoFixGuardError (env,RecCallInTypeOfDef c))
 	    else
 	      raise (CoFixGuardError (env,UnguardedRecursiveCall c))
@@ -917,32 +906,32 @@ let check_one_cofix env nbfix def deftype =
               if (noccur_with_meta n nbfix tm) then
 		if (List.for_all (noccur_with_meta n nbfix) args) then
 		  Array.iter (check_rec_call env alreadygrd n vlra) vrest
-		else 
+		else
 		  raise (CoFixGuardError (env,RecCallInCaseFun c))
-              else 
+              else
 		raise (CoFixGuardError (env,RecCallInCaseArg c))
-            else 
+            else
 	      raise (CoFixGuardError (env,RecCallInCasePred c))
-              
+
 	| Meta _ -> ()
         | Evar _ ->
 	    List.iter (check_rec_call env alreadygrd n vlra) args
-	      
-	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in 
+
+	| _    -> raise (CoFixGuardError (env,NotGuardedForm t)) in
 
   let (mind, _) = codomain_is_coind env deftype in
   let vlra = lookup_subterms env mind in
   check_rec_call env false 1 (dest_subterms vlra) def
 
-(* The  function which checks that the whole block of definitions 
+(* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env (bodynum,(names,types,bodies as recdef)) = 
-  let nbfix = Array.length bodies in 
+let check_cofix env (bodynum,(names,types,bodies as recdef)) =
+  let nbfix = Array.length bodies in
   for i = 0 to nbfix-1 do
     let fixenv = push_rec_types recdef env in
     try check_one_cofix fixenv nbfix bodies.(i) types.(i)
-    with CoFixGuardError (errenv,err) -> 
-      error_ill_formed_rec_body errenv err names i 
+    with CoFixGuardError (errenv,err) ->
+      error_ill_formed_rec_body errenv err names i
 	fixenv (judgment_of_fixpoint recdef)
   done