From b608b4ab69d0d4a2f2fc057877b582ffede45ed6 Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 29 Jan 2008 10:31:39 +0000
Subject: Correction du bug #1785

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

diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index b0e6b6ecff..6cde1ddcf5 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/contrib/rtauto/refl_tauto.ml
@@ -292,7 +292,7 @@ let rtauto_tac gls=
   let prf = 
     try project (search_fun (init_state [] formula)) 
     with Not_found ->
-      errorlabstrm "rtauto" (Pp.str "rtauto could'nt find any proof") in
+      errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
-- 
cgit v1.2.3