diff options
| author | Matthieu Sozeau | 2014-09-04 21:52:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-05 10:01:07 +0200 |
| commit | 8c54bdeec740fb9edd80e28ce743418bf1276b90 (patch) | |
| tree | 744cea8877f75bb440a61d815af6c59821f9cc65 /kernel | |
| parent | 080167469f6435696d785caa1fca9fd258148157 (diff) | |
Fix primitive projections declarations for inductive records.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/indtypes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 759d712061..2e9a81d98f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -781,16 +781,17 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re match isrecord with | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 -> (** The elimination criterion ensures that all projections can be defined. *) - let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in let u = if p then subst_univs_level_instance subst (Univ.UContext.instance ctx) else Univ.Instance.empty in + let indsp = ((kn, 0), u) in + let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections ((kn, 0), u) pkt.mind_typename nparamargs params + compute_projections indsp pkt.mind_typename nparamargs params pkt.mind_consnrealdecls pkt.mind_consnrealargs fields in Some (kns, projs) with UndefinableExpansion -> Some ([||], [||])) |