diff options
| author | amahboub | 2013-08-23 11:08:02 +0000 |
|---|---|---|
| committer | amahboub | 2013-08-23 11:08:02 +0000 |
| commit | 9fbe74a0799625fb2f43ec503b2ba8c89bb5aaea (patch) | |
| tree | 8f1046005e075df0be58f31247d30525ba8bd70d | |
| parent | c3f233d95a8454155204f3cf425bc5c021de7e92 (diff) | |
Updating documentation of the ring/field tactics.
Removes the requirements that are obsolete after commit r16730.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16731 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/Polynom.tex | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 8cd3488884..a2c09b8245 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -252,13 +252,7 @@ where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set, {\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is an implementation of this equality, and {\tt [x]} is a notation for -the image of {\tt x} by the ring morphism. Moreover, the term -{\tt [c0]} (resp. {\tt [c1]}), image by the morphism of the 0 -(resp. the 1) of the coefficient set, -should be \emph{convertible} to the term {\tt 0} (resp. the term -{\tt 1}) of the ring structure. This requirement is not enforced by -the command registering a new ring but the tactic is otherwise very -much incomplete. +the image of {\tt x} by the ring morphism. |