From 2dfb47c13d6f79fd44bd5f224873f84a6c00c8a9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 4 Mar 2006 23:44:25 +0000
Subject: Correction message d'erreur ltac et adoption du modèle de message de
 Tacinterp

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

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8a91cf61e4..7d0c926fac 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -20,6 +20,7 @@ open Environ
 open Type_errors
 open Typeops
 open Libnames
+open Nameops
 open Classops
 open List
 open Recordops 
@@ -121,7 +122,7 @@ let pretype_id loc env (lvar,unbndltacvars) id =
   try (* To build a nicer ltac error message *)
     match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"",
-	  str (string_of_id id ^ " ist not bound to a term"))
+	str "variable " ++ pr_id id ++ str " should be bound to a term")
       | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
   with Not_found ->
     error_var_not_found_loc loc id
-- 
cgit v1.2.3