From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- kernel/inductive.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'kernel/inductive.ml') diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 0f0dc0d60..e81a1cb58 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) = Vars.subst_instance_context u mib.mind_params_ctxt let instantiate_inductive_constraints mib u = - if mib.mind_polymorphic then - Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes)) - else Univ.Constraint.empty + let process auctx = + Univ.UContext.constraints (Univ.subst_instance_context u auctx) + in + match mib.mind_universes with + | Monomorphic_ind _ -> Univ.Constraint.empty + | Polymorphic_ind auctx -> process auctx + | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi) (************************************************************************) -- cgit v1.2.3