From 7a4e7dfbaa8dc3fa92931c4bfa39d268940e08f8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 Apr 2020 23:06:35 +0200
Subject: Remove mod_constraints field of module body

---
 kernel/mod_typing.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/mod_typing.mli')

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index fd5421aefe..94a4b17df3 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -23,13 +23,13 @@ open Names
 *)
 
 val translate_module :
-  env -> ModPath.t -> inline -> module_entry -> module_body
+  env -> ModPath.t -> inline -> module_entry -> module_body * Univ.Constraint.t
 
 (** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
     cannot be [None] (and of course [mod_expr] is [Abstract]). *)
 
 val translate_modtype :
-  env -> ModPath.t -> inline -> module_type_entry -> module_type_body
+  env -> ModPath.t -> inline -> module_type_entry -> module_type_body * Univ.Constraint.t
 
 (** Low-level function for translating a module struct entry :
     - We translate to a module when a [ModPath.t] is given,
@@ -39,7 +39,7 @@ val translate_modtype :
       the extraction. *)
 
 type 'alg translation =
-  module_signature * 'alg * delta_resolver * Univ.ContextSet.t
+  module_signature * 'alg * delta_resolver * Univ.Constraint.t
 
 val translate_mse :
   env -> ModPath.t option -> inline -> module_struct_entry ->
@@ -51,7 +51,7 @@ val translate_mse :
 val finalize_module :
   env -> ModPath.t -> (module_expression option) translation ->
   (module_type_entry * inline) option ->
-  module_body
+  module_body * Univ.Constraint.t
 
 (** [translate_mse_incl] translate the mse of a module or
     module type given to an Include *)
-- 
cgit v1.2.3