From e23ce63217dea3dcd1a760b44d774ad81f01a202 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Apr 2001 03:05:59 +0000
Subject: MAJ decompose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8182 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-tac.tex | 2 ++
 1 file changed, 2 insertions(+)

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}
-- 
cgit v1.2.3