From 601ce3738253e4bb197900ee6dad271c4e3666d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 14:23:25 +0200
Subject: Adding universe names to polymorphic entry instances.

---
 vernac/comInductive.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'vernac/comInductive.ml')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5ff3032ec4..0c39458a57 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   in
   let univs =
     match uctx with
-    | Polymorphic_const_entry uctx ->
+    | Polymorphic_const_entry (nas, uctx) ->
       if cum then
-        Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
-      else Polymorphic_ind_entry uctx
+        Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
+      else Polymorphic_ind_entry (nas, uctx)
     | Monomorphic_const_entry uctx ->
       Monomorphic_ind_entry uctx
   in
-- 
cgit v1.2.3