From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Tue, 28 Mar 2017 19:24:02 +0200
Subject: Extend definition of inductives to include subtyping info

---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 7d0edbc8b3..06eeeeab56 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -352,7 +352,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = Decl_kinds.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
-  mind_entry_universes = Univ.UContext.empty;
+  mind_entry_universes = (Univ.UContext.empty, Univ.UContext.empty);
   mind_entry_private = None;
 })
 
-- 
cgit v1.2.3