From c3318ad8408b1ceb0bfd4c2bfedec63ce9324698 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 5 Jun 2018 14:59:15 +0200 Subject: Change the proj_ind field from MutInd.t to inductive. This is a first step towards the acceptance of mutual record types in the kernel. --- kernel/nativecode.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/nativecode.ml') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8257dc8b8..914168695 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1965,6 +1965,7 @@ let compile_mind prefix ~interactive mb mind stack = in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in let add_proj j acc pb = + let () = assert (eq_ind ind pb.proj_ind) in let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -1985,7 +1986,7 @@ let compile_mind prefix ~interactive mb mind stack = let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in let code = MLlet(cf_uid, MLapp (MLprimitive Force_cofix, [|MLlocal c_uid|]), code) in - let gn = Gproj ("", (pb.proj_ind, j), pb.proj_arg) in + let gn = Gproj ("", ind, pb.proj_arg) in Glet (gn, mkMLlam [|c_uid|] code) :: acc in let projs = match mb.mind_record with @@ -2052,7 +2053,7 @@ let compile_deps env sigma prefix ~interactive init t = | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let pb = lookup_projection p env in - let init = compile_mind_deps env prefix ~interactive init pb.proj_ind in + let init = compile_mind_deps env prefix ~interactive init (fst pb.proj_ind) in aux env lvl init c | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in -- cgit v1.2.3