From a4839aa1ff076a8938ca182615a93d6afe748860 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 4 Jun 2018 13:32:35 +0200 Subject: Remove the proj_eta field of the kernel. This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel. --- interp/declare.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'interp') diff --git a/interp/declare.ml b/interp/declare.ml index 39c83f47e..aa737239b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -383,10 +383,12 @@ let inInductive : inductive_obj -> obj = rebuild_function = infer_inductive_subtyping } let declare_projections univs mind = - let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in + let env = Global.env () in + let spec,_ = Inductive.lookup_mind_specif env (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pbs)) -> - Array.iter2 (fun kn pb -> + | Some (Some (_, kns, _)) -> + let projs = Inductiveops.compute_projections env (mind, 0) in + Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in let univs = match univs with | Monomorphic_ind_entry _ -> @@ -398,16 +400,15 @@ let declare_projections univs mind = Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) in let term, types = match univs with - | Monomorphic_const_entry _ -> pb.proj_eta + | Monomorphic_const_entry _ -> term, types | Polymorphic_const_entry ctx -> let u = Univ.UContext.instance ctx in - let term, types = pb.proj_eta in Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in let entry = definition_entry ~types ~univs term in let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in assert (Constant.equal kn kn') - ) kns pbs; + ) kns projs; true, true | Some None -> true,false | None -> false,false -- cgit v1.2.3