From 2f3cd62d5118efe95330ddc06fdb43ee717ef993 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Sep 2017 16:07:34 +0200 Subject: Fixing #5755 (discharging of inductive types not correct with let-ins). The number of effective parameters was used where the number of declarations in the signature of parameters should have been used. --- vernac/discharge.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'vernac') diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 474c0b4dd..4a68fd138 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -36,7 +36,7 @@ let detype_param = I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] *) -let abstract_inductive hyps nparams inds = +let abstract_inductive hyps nparamdecls inds = let ntyp = List.length inds in let nhyp = Context.Named.length hyps in let args = Context.Named.to_instance mkVar (List.rev hyps) in @@ -50,18 +50,18 @@ let abstract_inductive hyps nparams inds = let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in (tname,arity',template,cnames,lc'')) inds in - let nparams' = nparams + Array.length args in + let nparamdecls' = nparamdecls + Array.length args in (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in - let (params,_) = decompose_prod_n_assum nparams' arity in + let (params,_) = decompose_prod_n_assum nparamdecls' arity in List.map detype_param params in let ind'' = List.map (fun (a,arity,template,c,lc) -> - let _, short_arity = decompose_prod_n_assum nparams' arity in + let _, short_arity = decompose_prod_n_assum nparamdecls' arity in let shortlc = - List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in + List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in { mind_entry_typename = a; mind_entry_arity = short_arity; mind_entry_template = template; @@ -79,7 +79,7 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let process_inductive (sechyps,_,_ as info) modlist mib = let sechyps = Lib.named_of_variable_context sechyps in - let nparams = mib.mind_nparams in + let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx @@ -106,7 +106,7 @@ let process_inductive (sechyps,_,_ as info) modlist mib = Array.to_list lc)) mib.mind_packets in let sechyps' = Context.Named.map discharge sechyps in - let (params',inds') = abstract_inductive sechyps' nparams inds in + let (params',inds') = abstract_inductive sechyps' nparamdecls inds in let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None -- cgit v1.2.3 From 22a3a79f32d5f795143bd808810aba890c630313 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 23 Sep 2017 16:18:10 +0200 Subject: Discharge.ml: cosmetic renaming of some variables. The point is to emphasize stronglier when we are talking about contexts or about arguments. --- vernac/discharge.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'vernac') diff --git a/vernac/discharge.ml b/vernac/discharge.ml index 4a68fd138..0e4bbd299 100644 --- a/vernac/discharge.ml +++ b/vernac/discharge.ml @@ -36,18 +36,18 @@ let detype_param = I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)] *) -let abstract_inductive hyps nparamdecls inds = +let abstract_inductive decls nparamdecls inds = let ntyp = List.length inds in - let nhyp = Context.Named.length hyps in - let args = Context.Named.to_instance mkVar (List.rev hyps) in + let ndecls = Context.Named.length decls in + let args = Context.Named.to_instance mkVar (List.rev decls) in let args = Array.of_list args in - let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in + let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in let inds' = List.map (function (tname,arity,template,cnames,lc) -> let lc' = List.map (substl subs) lc in - let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in - let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in + let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b decls) lc' in + let arity' = Termops.it_mkNamedProd_wo_LetIn arity decls in (tname,arity',template,cnames,lc'')) inds in let nparamdecls' = nparamdecls + Array.length args in @@ -77,8 +77,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Type ar.template_level), true -let process_inductive (sechyps,_,_ as info) modlist mib = - let sechyps = Lib.named_of_variable_context sechyps in +let process_inductive (section_decls,_,_ as info) modlist mib = + let section_decls = Lib.named_of_variable_context section_decls in let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with @@ -105,8 +105,8 @@ let process_inductive (sechyps,_,_ as info) modlist mib = Array.to_list mip.mind_consnames, Array.to_list lc)) mib.mind_packets in - let sechyps' = Context.Named.map discharge sechyps in - let (params',inds') = abstract_inductive sechyps' nparamdecls inds in + let section_decls' = Context.Named.map discharge section_decls in + let (params',inds') = abstract_inductive section_decls' nparamdecls inds in let record = match mib.mind_record with | Some (Some (id, _, _)) -> Some (Some id) | Some None -> Some None -- cgit v1.2.3