From 9fbe74a0799625fb2f43ec503b2ba8c89bb5aaea Mon Sep 17 00:00:00 2001
From: amahboub
Date: Fri, 23 Aug 2013 11:08:02 +0000
Subject: 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
---
 doc/refman/Polynom.tex | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

(limited to 'doc')

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