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/subtyping.ml | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'kernel/subtyping.ml')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 3f153ac244..a9403a5e34 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -306,11 +306,7 @@ let rec check_modules cst env msid1 l msb1 msb2 =
 and check_signatures cst env (msid1,sig1) (msid2,sig2') = 
   let mp1 = MPself msid1 in
   let env = add_signature mp1 sig1 env in 
-  let sig2 = try
-    subst_signature_msid msid2 mp1 sig2' 
-  with
-    | Circularity l -> 
-	error_circularity_in_subtyping l (string_of_msid msid1) (string_of_msid msid2) in
+  let sig2 = subst_signature_msid msid2 mp1 sig2' in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
-- 
cgit v1.2.3