diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-tac.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex index 5f82ef8f69..eb1d65d81a 100644 --- a/doc/RefMan-tac.tex +++ b/doc/RefMan-tac.tex @@ -955,6 +955,8 @@ Intros A B C H; Decompose [and or] H; Assumption. Qed. \end{coq_example*} +{\tt Decompose} does not work on right-hand sides of implications or products. + \begin{Variants} \item {\tt Decompose Sum \term}\tacindex{Decompose Sum} |