From ebb53e68cdc935a85c4da10852be4f7f3b492ee2 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 16 Jul 2015 16:40:25 +0200
Subject: Modules: fix bug #4294

We were throwing away constraints from 'with Definition' in module
type ascriptions.
---
 kernel/mod_typing.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26dd45f5f3..4f20e5f62a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -307,7 +307,9 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
-      mod_constraints = cst +++ cst' }
+      (** cst from module body typing, cst' from subtyping, 
+          and constraints from module type. *)
+      mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
-- 
cgit v1.2.3