From cfa3aa27f1141fe732a473efd0cff794694c63bb Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 21 Feb 2007 13:54:58 +0000
Subject: Fixed the pseudo-cicularity problem due to the with operator on
 Module Type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9662 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_typing.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 824d2e4eb5..e9bca90650 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -63,7 +63,8 @@ let rec translate_modtype env mte =
 
 and merge_with env mtb with_decl = 
   let msid,sig_b = match (Modops.scrape_modtype env mtb) with 
-    | MTBsig(msid,sig_b) -> msid,sig_b 
+    | MTBsig(msid,sig_b) -> let msid'=(refresh_msid msid) in
+	msid',(subst_signature_msid msid (MPself(msid')) sig_b)
     | _ -> error_signature_expected mtb
   in
   let id,idl = match with_decl with 
@@ -116,15 +117,6 @@ and merge_with env mtb with_decl =
 	      | _ -> error_not_a_module (string_of_label l)
 	    in
 	    let mtb = type_modpath env' mp in
-	 (* here, using assertions in substitutions, 
-	    we check that there is no msid bound in mtb *)
-	    begin
-	      try 
-		let _ = subst_modtype  (map_msid msid (MPself msid)) mtb in
-		  ()
-	      with
-		  Circularity _ -> error_circular_with_module id
-	    end;
 	    let cst =
               try check_subtypes env' mtb old.msb_modtype
               with Failure _ -> error_with_incorrect (label_of_id id) in
-- 
cgit v1.2.3