diff options
| -rw-r--r-- | interp/declare.ml | 34 | ||||
| -rw-r--r-- | kernel/entries.ml | 5 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 26 |
3 files changed, 25 insertions, 40 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index bc2d2068a..39c83f47e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -382,17 +382,33 @@ let inInductive : inductive_obj -> obj = discharge_function = discharge_inductive; rebuild_function = infer_inductive_subtyping } -let declare_projections mind = +let declare_projections univs mind = let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, pbs)) -> + Array.iter2 (fun kn pb -> let id = Label.to_id (Constant.label kn) in - let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) - in - assert(Constant.equal kn kn')) kns; true,true + let univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + Polymorphic_const_entry ctx + | Cumulative_ind_entry ctx -> + Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + in + let term, types = match univs with + | Monomorphic_const_entry _ -> pb.proj_eta + | 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; + true, true | Some None -> true,false | None -> false,false @@ -403,7 +419,7 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isrecord,isprim = declare_projections mind in + let isrecord,isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7e..3c555f8c7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.Named.t option * types in_constant_universes_entry * inline -type projection_entry = { - proj_entry_ind : MutInd.t; - proj_entry_arg : int } - type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry - | ProjectionEntry of projection_entry (** {6 Modules } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d29f2ca82..37bf679c5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -346,32 +346,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = cook_context = c.const_entry_secctx; } - | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (Some (id, kns, pbs)) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | _ -> assert false - in - let univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Monomorphic_const ctx - | Polymorphic_ind auctx -> Polymorphic_const auctx - | Cumulative_ind acumi -> - Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) - in - let term, typ = pb.proj_eta in - { - Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); - cook_type = typ; - cook_universes = univs; - cook_inline = false; - cook_context = None; - } - let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = |