From ee43b8005b283750c4ef6c1d2b537b8db9f9e24c Mon Sep 17 00:00:00 2001
From: soubiran
Date: Tue, 30 Jan 2007 12:46:36 +0000
Subject: Petite correction sur un message d'erreur renvoyé au sous typage.

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

(limited to 'kernel')

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 98ec21eaaa..3f153ac244 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -310,14 +310,14 @@ and check_signatures cst env (msid1,sig1) (msid2,sig2') =
     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
+	error_circularity_in_subtyping l (string_of_msid msid1) (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_sub l (debug_string_of_msid msid1) (debug_string_of_msid msid2)
+	  Not_found -> error_no_such_label_sub l (string_of_msid msid1) (string_of_msid msid2)
     in
       match spec2 with
 	| SPBconst cb2 ->
-- 
cgit v1.2.3