1 files changed, 1 insertions, 0 deletions
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;
       }