diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ff552c7caf..2c4ca46343 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -453,12 +453,7 @@ let build_branch_type env sigma dep p cs = let compute_projections env (kn, i as ind) = let open Term in let mib = Environ.lookup_mind kn env in - let u = match mib.mind_universes with - | Monomorphic_ind _ -> Instance.empty - | Polymorphic_ind auctx -> make_abstract_instance auctx - | Cumulative_ind acumi -> - make_abstract_instance (ACumulativityInfo.univ_context acumi) - in + let u = make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let x = match mib.mind_record with | NotRecord | FakeRecord -> anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") |