modifications des messages d'erreurs renvoyés lors de la comparaison

de deux signatures de modules.


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

1 files changed, 8 insertions, 2 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 537c20aef2..98ec21eaaa 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -22,6 +22,8 @@ open Mod_subst
 open Entries
 (*i*)
 
+
+
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
@@ -304,14 +306,18 @@ 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 = subst_signature_msid msid2 mp1 sig2' in
+  let sig2 = try
+    subst_signature_msid msid2 mp1 sig2' 
+  with
+    | Circularity l -> 
+	error_circularity_in_subtyping l (debug_string_of_msid msid1) (debug_string_of_msid msid2) in
   let map1 = make_label_map mp1 sig1 in
   let check_one_body cst (l,spec2) = 
     let info1 = 
       try 
 	Labmap.find l map1 
       with 
-	  Not_found -> error_no_such_label l 
+	  Not_found -> error_no_such_label_sub l (debug_string_of_msid msid1) (debug_string_of_msid msid2)
     in
       match spec2 with
 	| SPBconst cb2 ->