From 2c8ad1f81c486115fad58553ed15e775ca50de87 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 26 Oct 2011 16:22:35 +0000 Subject: Checker/subtyping.ml: avoid adding in env a module already there (fix #2609) When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1] in the environment. But since the stricter checks of commit r14150, this is an error if the environment already knows [mtb1] (for instance when doing (F M) and checking that M is compatible with the type of the arg of F. [check_subtypes] now expect [mtb1] to be already in env, and we move the add_module to the unique call site of this function that requires it. Moreover, we solve a second issue : when subtyping a functor, we update the environment once inside the functor, and this is also refused by the checks of commits r14150. So we first remove the module name from the env before doing the update. Since the module added earlier was a functor, there is no inner defs to chase in env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/subtyping.mli | 3 +++ 1 file changed, 3 insertions(+) (limited to 'checker/subtyping.mli') diff --git a/checker/subtyping.mli b/checker/subtyping.mli index 07f48789d..ecdf55775 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -13,6 +13,9 @@ open Declarations open Environ (*i*) +(** Invariant: the first [module_type_body] is now supposed to be + known by [env] *) + val check_subtypes : env -> module_type_body -> module_type_body -> unit -- cgit v1.2.3