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

---
 API/API.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 69278e7c9f..e2c43dab82 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1094,6 +1094,7 @@ sig
         mind_params_ctxt : Context.Rel.t;
         mind_polymorphic : bool;
         mind_universes : Univ.UContext.t;
+        mind_subtyping : Univ.universe_context;
         mind_private : bool option;
         mind_typing_flags : Declarations.typing_flags;
       }
-- 
cgit v1.2.3