From 5ed282074f59cd3fc447eafbca4eba5769d42710 Mon Sep 17 00:00:00 2001
From: thery
Date: Wed, 7 Feb 2007 13:50:53 +0000
Subject: Field rewrites only with polynomial

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9607 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/Polynom.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc')

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