diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declareops.ml | 8 | ||||
| -rw-r--r-- | kernel/entries.mli | 3 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 23 |
3 files changed, 21 insertions, 13 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 51b7b6f97..9d2382f6e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -223,8 +223,14 @@ 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 (c, ps as r) = + let c' = subst_mps sub c in + let ps' = Array.smartmap (subst_constant sub) ps in + if c' == c && ps' == ps then r + else (c', ps') + let subst_mind_body sub mib = - { mind_record = mib.mind_record ; + { mind_record = Option.smartmap (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); diff --git a/kernel/entries.mli b/kernel/entries.mli index c672ba731..244637acd 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -41,7 +41,8 @@ type one_inductive_entry = { mind_entry_lc : constr list } type mutual_inductive_entry = { - mind_entry_record : bool; + mind_entry_record : bool option; + (** Some true: primitive record, Some false: non-primitive record *) mind_entry_finite : bool; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 6e87a0444..9c83ba1a9 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -742,17 +742,18 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re } in let packets = Array.map2 build_one_packet inds recargs in let isrecord = - let pkt = packets.(0) in - if isrecord (* || (Array.length pkt.mind_consnames = 1 && *) - (* inductive_sort_family pkt <> InProp) *) then - let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in - let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in - try - let exp = compute_expansion ((kn, 0), u) params - (List.firstn pkt.mind_consnrealdecls.(0) rctx) - in Some exp - with UndefinableExpansion -> None - else None + match isrecord with + | Some true -> (* || (Array.length pkt.mind_consnames = 1 && *) + let pkt = packets.(0) in + let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in + let u = if p then Univ.UContext.instance ctx else Univ.Instance.empty in + (try + let exp = compute_expansion ((kn, 0), u) params + (List.firstn pkt.mind_consnrealdecls.(0) rctx) + in Some exp + with UndefinableExpansion -> (Some (mkProp, [||]))) + | Some false -> Some (mkProp, [||]) + | None -> None in (* Build the mutual inductive *) { mind_record = isrecord; |