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
---
 proofs/tacinterp.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index c98840d731..9f68b896fe 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -186,12 +186,12 @@ let glob_const_nvar loc env qid =
   try
     (* We first look for a variable of the current proof *)
     match repr_qualid qid with
-      | [],s ->
-	  let id = id_of_string s in
+      | [],id ->
 	  (* lookup_value may raise Not_found *)
 	  (match Environ.lookup_named_value id env with
 	     | Some _ -> EvalVarRef id
-	     | None -> error (s^" does not denote an evaluable constant"))
+	     | None -> error ((string_of_id id)^
+			      " does not denote an evaluable constant"))
       | _ -> raise Not_found
   with Not_found ->
   try
-- 
cgit v1.2.3