aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/inv.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2a11d6520..eb978ba48 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -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