Correction d'un bug sur les modules de la forme:

Module F (X : S) : F_sig X.
...
End F.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10702 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 7 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 6074bac9c..01450599a 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -644,13 +644,6 @@ let end_module id =
 
   let oldoname,oldprefix,fs,lib_stack = Lib.end_module id in
   let mbids, res_o, sub_o = !openmod_info in
-  let mp = Global.end_module id res_o in
-    
-  begin match sub_o with
-      None -> ()
-    | Some sub_mtb -> check_subtypes mp sub_mtb
-  end;
-    
   let substitute, keep, special = Lib.classify_segment lib_stack in
 
   let dir = fst oldprefix in
@@ -674,6 +667,14 @@ let end_module id =
 
     (* must be called after get_modtype_substobjs, because of possible
      dependencies on functor arguments *)
+
+  let mp = Global.end_module id res_o in
+    
+  begin match sub_o with
+      None -> ()
+    | Some sub_mtb -> check_subtypes mp sub_mtb
+  end;
+    
   Summary.module_unfreeze_summaries fs;
 
   let substituted = subst_substobjs dir mp substobjs in