diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 8e9b606a58..b117f8714b 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -710,7 +710,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( best-effort fashion. *) let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in - let recursive = finite != Decl_kinds.BiFinite in + let recursive = finite != BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in let ra_env_ar = Array.rev_to_list rc in let nparamsctxt = Context.Rel.length paramsctxt in @@ -879,9 +879,13 @@ let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx) + let (inst, auctx) = Univ.abstract_universes ctx in + let inst = Univ.make_instance_subst inst in + (inst, Polymorphic_ind auctx) | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi) + let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + let inst = Univ.make_instance_subst inst in + (inst, Cumulative_ind acumi) let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in |