From 3c248785237d8dea037da274f4acc0229894de93 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Feb 2001 15:58:48 +0000
Subject: ident au lieu de string pour le nom de base de qualid

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pretty.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'parsing/pretty.ml')

diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index af94577af2..34d3d29803 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -416,9 +416,8 @@ let print_name qid =
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
     if dir <> [] then raise Not_found;
-    let name = id_of_string str in
-    let (c,typ) = Global.lookup_named name in 
-    [< print_named_decl (name,c,typ) >]
+    let (c,typ) = Global.lookup_named str in 
+    [< print_named_decl (str,c,typ) >]
   with Not_found ->
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
-- 
cgit v1.2.3