From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 kernel/inductive.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c62d0e7ded..848ae65c51 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -56,12 +56,7 @@ let inductive_paramdecls (mib,u) =
   Vars.subst_instance_context u mib.mind_params_ctxt
 
 let instantiate_inductive_constraints mib u =
-  let process auctx =  Univ.AUContext.instantiate 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)
-
+  Univ.AUContext.instantiate u (Declareops.inductive_polymorphic_context mib)
 
 (************************************************************************)
 
-- 
cgit v1.2.3