diff options
Diffstat (limited to 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 1b73096f7..3e6c4858e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -84,7 +84,7 @@ let subst_const_def sub def = match def with | OpaqueDef o -> OpaqueDef (Opaqueproof.subst_opaque sub o) let subst_const_proj sub pb = - { pb with proj_ind = subst_mind sub pb.proj_ind; + { pb with proj_ind = subst_ind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; } @@ -208,14 +208,21 @@ let subst_mind_packet sub mbp = mind_nb_args = mbp.mind_nb_args; mind_reloc_tbl = mbp.mind_reloc_tbl } -let subst_mind_record sub (id, ps, pb as r) = - let ps' = Array.Smart.map (subst_constant sub) ps in - let pb' = Array.Smart.map (subst_const_proj sub) pb in - if ps' == ps && pb' == pb then r +let subst_mind_record sub r = match r with +| NotRecord -> NotRecord +| FakeRecord -> FakeRecord +| PrimRecord infos -> + let map (id, ps, pb as info) = + let ps' = Array.Smart.map (subst_constant sub) ps in + let pb' = Array.Smart.map (subst_const_proj sub) pb in + if ps' == ps && pb' == pb then info else (id, ps', pb') + in + let infos' = Array.Smart.map map infos in + if infos' == infos then r else PrimRecord infos' let subst_mind_body sub mib = - { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ; + { mind_record = subst_mind_record sub mib.mind_record ; mind_finite = mib.mind_finite ; mind_ntypes = mib.mind_ntypes ; mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false); |