diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index d56502a095..da5217eb33 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -114,6 +114,7 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; const_private_poly_univs = cb.const_private_poly_univs; + const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -222,6 +223,7 @@ let subst_mind_packet sub mbp = mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); + mind_relevant = mbp.mind_relevant; mind_nb_constant = mbp.mind_nb_constant; mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } @@ -230,10 +232,10 @@ let subst_mind_record sub r = match r with | NotRecord -> NotRecord | FakeRecord -> FakeRecord | PrimRecord infos -> - let map (id, ps, pb as info) = + let map (id, ps, rs, pb as info) = let pb' = Array.Smart.map (subst_mps sub) pb in if pb' == pb then info - else (id, ps, pb') + else (id, ps, rs, pb') in let infos' = Array.Smart.map map infos in if infos' == infos then r else PrimRecord infos' @@ -269,21 +271,32 @@ let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with | NotRecord | FakeRecord -> None | PrimRecord infos -> + let _, labs, _, _ = infos.(snd ind) in Some (Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg - (pi2 infos.(snd ind)).(proj_arg)) + labs.(proj_arg)) let inductive_make_projections ind mib = match mib.mind_record with | NotRecord | FakeRecord -> None | PrimRecord infos -> + let _, labs, _, _ = infos.(snd ind) in let projs = Array.mapi (fun proj_arg lab -> Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab) - (pi2 infos.(snd ind)) + labs in Some projs +let relevance_of_projection_repr mib p = + let _mind,i = Names.Projection.Repr.inductive p in + match mib.mind_record with + | NotRecord | FakeRecord -> + CErrors.anomaly ~label:"relevance_of_projection" Pp.(str "not a projection") + | PrimRecord infos -> + let _,_,rs,_ = infos.(i) in + rs.(Names.Projection.Repr.arg p) + (** {6 Hash-consing of inductive declarations } *) let hcons_regular_ind_arity a = |