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 +++-
 kernel/univ.ml       | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

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) ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1d82be63b9..336cdb653e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -577,7 +577,7 @@ struct
   let is_type0m x = equal type0m x
   let is_type0 x = equal type0 x
 
-  (* Returns the formal universe that lies juste above the universe variable u.
+  (* Returns the formal universe that lies just above the universe variable u.
      Used to type the sort u. *)
   let super l = 
     if is_small l then type1
-- 
cgit v1.2.3