From 89a3416f68bddad29e80ed7d4f93b4a5ef418bd7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 28 Jul 2000 13:28:09 +0000
Subject: messages d'erreur

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

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0beab3f7a1..2c418bbae8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -363,7 +363,7 @@ let rec intros_until s g =
 	with UserError ("Term not reducible",_) ->
           errorlabstrm "Intros" 
 	    [<'sTR "No such hypothesis in current goal";
-	      'sTR "even after head-reduction" >]
+	      'sTR " even after head-reduction" >]
 
 let rec intros_until_n n g =
   match pf_lookup_index_as_renamed (pf_concl g) n with
@@ -374,7 +374,7 @@ let rec intros_until_n n g =
 	with UserError ("Term not reducible",_) ->
           errorlabstrm "Intros" 
 	    [<'sTR "No such hypothesis in current goal";
-	      'sTR "even after head-reduction" >]
+	      'sTR " even after head-reduction" >]
 
 let dyn_intros_until = function 
   | [Identifier id] -> intros_until id
-- 
cgit v1.2.3