From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 1 Jul 2010 17:21:14 +0200
Subject: Imported Upstream version 8.2pl2+dfsg

---
 tactics/inv.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics/inv.ml')

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 977b602e..af204e77 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
+(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls =
 let rec tclMAP_i n tacfun = function
   | [] -> tclDO n (tacfun None)
   | a::l -> 
-      if n=0 then error "Too much names."
+      if n=0 then error "Too many names."
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
 let remember_first_eq id x = if !x = no_move then x := MoveAfter id
-- 
cgit v1.2.3