diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7ae787d224..759d712061 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -782,7 +782,11 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re | 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 Univ.UContext.instance ctx else Univ.Instance.empty in + let u = + if p then + subst_univs_level_instance subst (Univ.UContext.instance ctx) + else Univ.Instance.empty + in (try let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in let kns, projs = |