From 4d17489394dbf6008e5abd5b8d075f08280cd38c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Mon, 29 Jan 2018 17:01:20 +0100
Subject: Extrude monomorphic universe contexts from with Definition
 constraints.

We defer the computation of the universe quantification to the upper layer,
outside of the kernel.
---
 library/declaremods.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library/declaremods.mli')

diff --git a/library/declaremods.mli b/library/declaremods.mli
index 42e5f4b13..0df55f34d 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -13,7 +13,7 @@ open Vernacexpr
 
 type 'modast module_interpretor =
   Environ.env -> Misctypes.module_kind -> 'modast ->
-    Entries.module_struct_entry * Misctypes.module_kind
+    Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t
 
 type 'modast module_params =
   (Id.t Loc.located list * ('modast * inline)) list
-- 
cgit v1.2.3