diff options
| author | Guillaume Melquiond | 2015-02-10 13:32:58 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-02-10 13:32:58 +0100 |
| commit | 85458847345fdad2236da0171f6f0860992a9493 (patch) | |
| tree | 1c0a0753db24458ef00fb0514c282fc55aeb6076 /doc | |
| parent | 804421f10f474d458a9bb8d62c67b97216f77aae (diff) | |
Fix documentation of generalize. (Fix for bug #4015)
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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 |