Legacy Ring and Legacy Field migrated to contribs

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

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

2 files changed, 0 insertions, 276 deletions

diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 664c0d3ff..a2f5197f9 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -637,281 +637,6 @@ apply. There is only one specific modifier:
   on coefficients w.r.t. the field equality.
 \end{description}
 
-\asection{Legacy implementation}
-
-\Warning This tactic is the {\tt ring} tactic of previous versions of
-\Coq{} and it should be considered as deprecated. It will probably be
-removed in future releases. It has been kept only for compatibility
-reasons and in order to help moving existing code to the newer
-implementation described above. For more details, please refer to the
-Coq Reference Manual, version 8.0.
-
-
-\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
-\tacindex{legacy ring}
-\comindex{Add Legacy Ring}
-\comindex{Add Legacy Semi Ring}}
-
-This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
-associative commutative rewriting on every ring.  The tactic must be
-loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
-the \texttt{Add Ring} command. The ring of booleans (with \texttt{andb}
-as multiplication and \texttt{xorb} as addition)
-is predefined; if one wants to use the tactic on \texttt{nat} one must
-first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
-\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require
-Import LegacyNArithRing}.
-
-The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
-conclusion. The tactic \texttt{ring} normalizes these terms
-w.r.t. associativity and commutativity and replace them by their
-normal form.
-
-\begin{Variants}
-\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
-  acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
-  solves the equality by reflexivity.
-
-\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
-    S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
-  proof that \texttt{forall (n:nat), S n = plus (S O) n}.
-
-\end{Variants}
-
-You can have a look at the files \texttt{LegacyRing.v},
-\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
-\texttt{Add Ring} command.
-
-\subsection{Add a ring structure}
-
-It can be done in the \Coq toplevel (No ML file to edit and to link
-with \Coq). First, \texttt{ring} can handle two kinds of structure:
-rings and semi-rings. Semi-rings are like rings without an opposite to
-addition. Their precise specification (in \gallina) can be found in
-the file
-
-\begin{quotation}
-\begin{verbatim}
-plugins/ring/Ring_theory.v
-\end{verbatim}
-\end{quotation}
-
-The typical example of ring is \texttt{Z}, the typical
-example of semi-ring is \texttt{nat}.
-
-The specification of a
-ring is divided in two parts: first the record of constants
-($\oplus$, $\otimes$, 1, 0, $\ominus$) and then the theorems
-(associativity, commutativity, etc.).
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_semi_rings.
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-(* There is also a "weakly decidable" equality on A. That means 
-  that if (A_eq x y)=true then x=y but x=y can arise when 
-  (A_eq x y)=false. On an abstract ring the function [x,y:A]false
-  is a good choice. The proof of A_eq_prop is in this case easy. *)
-Variable Aeq : A -> A -> bool.
-
-Record Semi_Ring_Theory : Prop :=
-{ SR_plus_sym  : (n,m:A)[| n + m == m + n |];
-  SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-
-  SR_mult_sym : (n,m:A)[| n*m == m*n |];
-  SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
-  SR_plus_zero_left :(n:A)[| 0 + n == n|];
-  SR_mult_one_left : (n:A)[| 1*n == n |];
-  SR_mult_zero_left : (n:A)[| 0*n == 0 |];
-  SR_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
-  SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
-  SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_rings.
-
-Variable A : Type.
-
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aopp : A -> A.
-Variable Aeq : A -> A -> bool.
-
-
-Record Ring_Theory : Prop :=
-{ Th_plus_sym  : (n,m:A)[| n + m == m + n |];
-  Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-  Th_mult_sym : (n,m:A)[| n*m == m*n |];
-  Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
-  Th_plus_zero_left :(n:A)[| 0 + n == n|];
-  Th_mult_one_left : (n:A)[| 1*n == n |];
-  Th_opp_def : (n:A) [| n + (-n) == 0 |];
-  Th_distr_left   : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
-  Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-To define a ring structure on A, you must provide an addition, a
-multiplication, an opposite function and two unities 0 and 1.
-
-You must then prove all theorems that make
-(A,Aplus,Amult,Aone,Azero,Aeq) 
-a ring structure, and pack them with the \verb|Build_Ring_Theory| 
-constructor.
-
-Finally to register a ring the syntax is:
-
-\comindex{Add Legacy Ring}
-\begin{quotation}
-  \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
-  \texttt{[} \textit{c1 \dots cn} \texttt{].}
-\end{quotation}
-
-\noindent where \textit{A} is a term of type \texttt{Set}, 
-\textit{Aplus} is a term of type \texttt{A->A->A},
-\textit{Amult} is a term of type \texttt{A->A->A},
-\textit{Aone} is a term of type \texttt{A},
-\textit{Azero} is a term of type \texttt{A},
-\textit{Ainv} is a term of type \texttt{A->A},
-\textit{Aeq} is a term of type \texttt{A->bool},
-\textit{T} is a term of type 
-\texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv
-  Aeq}\texttt{)}.
-The arguments \textit{c1 \dots cn}, 
-are the names of constructors which define closed terms: a
-subterm will be considered as a constant if it is either one of the
-terms \textit{c1 \dots cn} or the application of one of these terms to
-closed terms. For \texttt{nat}, the given constructors are \texttt{S}
-and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
-\texttt{(S (S O))}, \ldots
-
-\begin{Variants}
-\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} 
-  \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
-    Ring}
-  
-  There are two differences with the \texttt{Add Ring} command: there
-  is no inverse function and the term $T$ must be of type
-  \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
-    Aeq}\texttt{)}.
-
-\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv 
-    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
-  
-  This command should be used for when the operations of rings are not
-  computable; for example the real numbers of
-  \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but
-  you still may want to \textit{rewrite} it to $1$ using the ring
-  axioms. The argument \texttt{Aeq} is not used; a good choice for
-  that function is \verb+[x:A]false+.
-
-\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
-    Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Not a valid (semi)ring theory}.
- 
-  That happens when the typing condition does not hold.
-\end{ErrMsgs}
-
-Currently, the hypothesis is made than no more than one ring structure
-may be declared for a given type in \texttt{Set} or \texttt{Type}.
-This allows automatic detection of the theory used to achieve the
-normalization. On popular demand, we can change that and allow several
-ring structures on the same set.
-
-The table of ring theories is compatible with the \Coq\ 
-sectioning mechanism. If you declare a ring inside a section, the
-declaration will be thrown away when closing the section.
-And when you load a compiled file, all the \texttt{Add Ring}
-commands of this file that are not inside a section will be loaded.
-
-The typical example of ring is \texttt{Z}, and the typical example of
-semi-ring is \texttt{nat}. Another ring structure is defined on the
-booleans. 
-
-\Warning Only the ring of booleans is loaded by default with the
-\texttt{Ring} module. To load the ring structure for \texttt{nat},
-load the module \texttt{ArithRing}, and for \texttt{Z},
-load the module \texttt{ZArithRing}.
-
-\subsection{\tt legacy field
-\tacindex{legacy field}}
-
-This tactic written by David~Delahaye and Micaela~Mayero solves equalities
-using commutative field theory. Denominators have to be non equal to zero and,
-as this is not decidable in general, this tactic may generate side conditions
-requiring some expressions to be non equal to zero. This tactic must be loaded
-by {\tt Require Import LegacyField}. Field theories are declared (as for
-{\tt legacy ring}) with
-the {\tt Add Legacy Field} command.
-
-\subsection{\tt Add Legacy Field
-\comindex{Add Legacy Field}}
-
-This vernacular command adds a commutative field theory to the database for the
-tactic {\tt field}. You must provide this theory as follows:
-\begin{flushleft}
-{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
-Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
-\end{flushleft}
-where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
-a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
-  A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
-    Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
-type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
-  {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
-of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
-and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
-  {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
-To build a ring theory, refer to Chapter~\ref{ring} for more details.
-
-This command adds also an entry in the ring theory table if this theory is not
-already declared. So, it is useless to keep, for a given type, the {\tt Add
-Ring} command if you declare a theory with {\tt Add Field}, except if you plan
-to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
-module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
-Require Import Ring} if you want to call the {\tt ring} tactic.
-
-\begin{Variants}
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with minus:={\it Aminus}}
-
-Adds also the term {\it Aminus} which must be a constant expressed by
-means of {\it Aopp}.
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Legacy Field }with div:={\it Adiv}}
-
-Adds also the term {\it Adiv} which must be a constant expressed by
-means of {\it Ainv}.
-
-\end{Variants}
-
-\SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
-legacy field}.
-
 \asection{History of \texttt{ring}}
 
 First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0bd402535..6ad232b5f 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -576,7 +576,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Reals/SeqSeries.v
     theories/Reals/Sqrt_reg.v
     theories/Reals/Rlogic.v
-    theories/Reals/LegacyRfield.v
     (theories/Reals/Reals.v)
   </dd>