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/termast.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'parsing/termast.ml')

diff --git a/parsing/termast.ml b/parsing/termast.ml
index b1a2d18d1f..026e79324a 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -94,7 +94,7 @@ let ast_of_ref = function
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
-  let args = List.map nvar (dir@[s]) in
+  let args = List.map nvar (dir@[string_of_id s]) in
   ope ("QUALID", args)
 
 (**********************************************************************)
@@ -179,7 +179,7 @@ let rec ast_of_raw = function
 	 | RVar (_,id) ->
 	     let imp =
 	       try 
-		 let ref = Nametab.locate (make_qualid [] (string_of_id id)) in
+		 let ref = Nametab.locate (make_qualid [] id) in
 		 implicits_of_global ref
 	       with Not_found -> [] in
 	     ast_of_app imp astf astargs
-- 
cgit v1.2.3