diff options
| author | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-18 13:09:14 +0100 |
| commit | a59574c8eb4bdda60e4bdd6197e8a32574985588 (patch) | |
| tree | e15e1a0f78d23cd263726d725c93a5e6ce453465 /pretyping/inductiveops.ml | |
| parent | f8d6c322783577b31cf55f8b55568ac56104202b (diff) | |
| parent | a9f0fd89cf3bb4b728eb451572a96f8599211380 (diff) | |
Merge PR #9439: Separate variance and universe fields in inductives.
Ack-by: ppedrot
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") |