diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f3b03252db..0f0dc0d607 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -55,7 +55,7 @@ let inductive_paramdecls (mib,u) = let instantiate_inductive_constraints mib u = if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints mib.mind_universes) + Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) else Univ.Constraint.empty |