From c0fd6794e39fb068c8180126568a33d0d670c7df Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 6 Dec 2000 11:47:12 +0000
Subject: message d'erreur

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 28e53c058b..b54fd0a630 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -693,7 +693,7 @@ let letin_tac with_eq name c occs gl =
   let id =
     if name = Anonymous then next_global_ident_away x used_ids else
       if not (mem_named_context x (named_context env)) then x else
-	error ("Variable "^(string_of_id x)^" is already declared") in
+	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
   let t = pf_type_of gl c in
   let heq = next_global_ident_away (id_of_string "Heq") used_ids in
-- 
cgit v1.2.3