From 4422432dd55c823595f31163c92306349769d3e4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 8 May 2016 16:52:02 +0200
Subject: Fix bug #4713: Anomaly: Assertion Failed for incorrect usage of
 Module.

---
 library/declaremods.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'library/declaremods.ml')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 651c76ae1..b3858146d 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -642,7 +642,11 @@ let declare_module interp_modast id args res mexpr_o fs =
   let env = Global.env () in
   let mty_entry_o, subs, inl_res = match res with
     | Enforce (mty,ann) ->
-        Some (fst (interp_modast env ModType mty)), [], inl2intopt ann
+        let inl = inl2intopt ann in
+        let mte, _ = interp_modast env ModType mty in
+        (* We check immediately that mte is well-formed *)
+        let _ = Mod_typing.translate_mse env None inl mte in
+        Some mte, [], inl
     | Check mtys ->
 	None, build_subtypes interp_modast env mp arg_entries_r mtys,
         default_inline ()
-- 
cgit v1.2.3