summaryrefslogtreecommitdiff
path: root/kernel/inductive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/inductive.ml')
-rw-r--r--kernel/inductive.ml241
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-24 17:48:48 +0000