From 4422432dd55c823595f31163c92306349769d3e4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot 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 +++++- test-suite/bugs/closed/4713.v | 10 ++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4713.v 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 () diff --git a/test-suite/bugs/closed/4713.v b/test-suite/bugs/closed/4713.v new file mode 100644 index 000000000..5d4d73be3 --- /dev/null +++ b/test-suite/bugs/closed/4713.v @@ -0,0 +1,10 @@ +Module Type T. + Parameter t : Type. +End T. +Module M : T. + Definition t := unit. +End M. + +Fail Module Z : T with Module t := M := M. +Fail Module Z <: T with Module t := M := M. +Fail Declare Module Z : T with Module t := M. -- cgit v1.2.3