Field rewrites only with polynomial

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9607 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 1 deletions

diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index f50a0e4f29..32142112c4 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -526,7 +526,9 @@ Reset Initial.
     {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
     where $m$ is a monomial (after ``abstraction''),
     $p$ a polynomial and $=$ the corresponding equality of the field structure.
-
+    Beware that rewriting works with the equality $m=p$ only if $p$ is a 
+    polynomial since rewriting is handled by the underlying {\tt ring}
+    tactic.
   \item {\tt field\_simplify} 
      performs the simplification in the conclusion of the goal, $F_1 = F_2$
      becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the