From 5f5eddc1779ccb0afd022d4b54ae6405d0439488 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Jul 2008 15:25:15 +0000
Subject: Autour du parsing: - Utilisation de notations de type "abbreviation
 paramétrée" plutôt que   de notations introduisant des mots-clés, là où c'est
 possible (cela affecte   QDen, in_left/in_right, inhabited, S/P dans
 NZCyclic). - Extension du lexeur pour qu'il prenne le plus long token valide
 au   lieu d'échouer sur un plus long préfixe non valide de token (permet  
 notamment de faire passer la notation de Georges "'C_ G ( A )"   sans
 invalider toute séquence commençant par 'C et non suivie de _) - Rajout d'un
 point final à certains messages d'erreur qui n'en avaient pas. - Ajout
 String.copy dans string_of_label ("trou" de mutabilité signalé   par Georges
 -- le "trou" lié aux vecteurs des noeuds App restant lui   ouvert).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 3d80ad23e8..0191880d16 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -103,7 +103,7 @@ let label_of_mbid (_,s,_) = s
 
 
 let mk_label l = l
-let string_of_label l = l
+let string_of_label = string_of_id
 
 let id_of_label l = l
 let label_of_id id = id
-- 
cgit v1.2.3