From aba21455f0d9e570106a8b4d9c1bd6241664f1d3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 9 Dec 2004 13:48:57 +0000 Subject: Amélioration message localisation constructions et modules MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6453 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/prettyp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'parsing/prettyp.ml') diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index e30823078..da915f17b 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -216,7 +216,7 @@ let print_located_qualid ref = (fun (o,oqid) -> hov 2 (pr_located_qualid o ++ (if oqid <> qid then - spc() ++ str "(visible as " ++ pr_qualid oqid ++ str")" + spc() ++ str "(shorter name to refer to it is " ++ pr_qualid oqid ++ str")" else mt ()))) l -- cgit v1.2.3