From 2dfb47c13d6f79fd44bd5f224873f84a6c00c8a9 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 4 Mar 2006 23:44:25 +0000
Subject: Correction message d'erreur ltac et adoption du modèle de message de
 Tacinterp
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 394d0ae13..608e1bc90 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -265,7 +265,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
   try
     match List.assoc id unbndltacvars with
       | None -> user_err_loc (loc,"intern_var",
-	  pr_id id ++ str " 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 ->
   (* Is [id] a goal or section variable *)
-- 
cgit v1.2.3