From 85458847345fdad2236da0171f6f0860992a9493 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 10 Feb 2015 13:32:58 +0100
Subject: Fix documentation of generalize. (Fix for bug #4015)

---
 doc/refman/RefMan-tac.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 33f6730e0a..ee40a0d51e 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1339,7 +1339,7 @@ in the list of subgoals remaining to prove.
 \label{generalize}
 
 This tactic applies to any goal. It generalizes the conclusion with
-respect to one of its subterms.
+respect to some term.
 
 \Example
 
-- 
cgit v1.2.3