From fe07a7f5f4b5b1d92e0e83cab9b886b642c6f8eb Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Fri, 30 Aug 2013 12:20:09 +0000
Subject: Fix typo in error message

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

(limited to 'plugins/funind')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7c70815a68..bac3ad45f0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1256,7 +1256,7 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" ->
-			     errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
+			     errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
 			     then
-- 
cgit v1.2.3