From 4d17489394dbf6008e5abd5b8d075f08280cd38c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot 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. --- interp/modintern.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/modintern.mli') diff --git a/interp/modintern.mli b/interp/modintern.mli index a21b6e231..8d6100667 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -28,4 +28,4 @@ exception ModuleInternalizationError of module_internalization_error isn't ModAny. *) val interp_module_ast : - env -> module_kind -> module_ast -> module_struct_entry * module_kind + env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t -- cgit v1.2.3