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

38 files changed, 12 insertions, 6687 deletions

diff --git a/Makefile.build b/Makefile.build
index 2aa4ca6d7..db977cb13 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -433,18 +433,16 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 # 3) plugins
 ###########################################################################
 
-.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction
-.PHONY: field fourier funind cc rtauto btauto pluginsopt
+.PHONY: plugins omega micromega setoid_ring nsatz xml extraction
+.PHONY: fourier funind cc rtauto btauto pluginsopt
 
 plugins: $(PLUGINSVO)
 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
 micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
-ring: $(RINGVO) $(RINGCMA)
-setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
+setoid_ring: $(RINGVO) $(RINGCMA)
 nsatz: $(NSATZVO) $(NSATZCMA)
 xml: $(XMLVO) $(XMLCMA)
 extraction: $(EXTRACTIONCMA)
-field: $(FIELDVO) $(FIELDCMA)
 fourier: $(FOURIERVO) $(FOURIERCMA)
 funind: $(FUNINDCMA) $(FUNINDVO)
 cc: $(CCVO) $(CCCMA)
diff --git a/Makefile.common b/Makefile.common
index 5ce5442f8..1ede03836 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -74,9 +74,9 @@ SRCDIRS:=\
   pretyping	interp		toplevel/utils	toplevel 	parsing \
   printing	grammar 	intf            ide/utils	ide	\
   $(addprefix plugins/, \
-    omega	romega 		micromega 	quote		ring \
+    omega	romega 		micromega 	quote \
     setoid_ring xml 		extraction 	fourier \
-    cc 		funind 		firstorder 	field \
+    cc 		funind 		firstorder \
     rtauto 	nsatz           syntax          decl_mode	btauto)
 
 # Order is relevent here because kernel and checker contain files
@@ -166,10 +166,8 @@ OMEGACMA:=plugins/omega/omega_plugin.cma
 ROMEGACMA:=plugins/romega/romega_plugin.cma
 MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
 QUOTECMA:=plugins/quote/quote_plugin.cma
-RINGCMA:=plugins/ring/ring_plugin.cma
-NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+RINGCMA:=plugins/setoid_ring/newring_plugin.cma
 NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-FIELDCMA:=plugins/field/field_plugin.cma
 XMLCMA:=plugins/xml/xml_plugin.cma
 FOURIERCMA:=plugins/fourier/fourier_plugin.cma
 EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
@@ -188,7 +186,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
 DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
 
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
-        $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
+        $(QUOTECMA) $(RINGCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
         $(CCCMA)  $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
         $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
@@ -300,9 +298,7 @@ OMEGAVO:=$(call cat_vo_itarget, plugins/omega)
 ROMEGAVO:=$(call cat_vo_itarget, plugins/romega)
 MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega)
 QUOTEVO:=$(call cat_vo_itarget, plugins/quote)
-RINGVO:=$(call cat_vo_itarget, plugins/ring)
-FIELDVO:=$(call cat_vo_itarget, plugins/field)
-NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
+RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
 NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
 FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
 FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
@@ -312,9 +308,9 @@ EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
 XMLVO:=
 CCVO:=
 
-PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
 	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(BTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \
+	    $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
             $(NSATZVO) $(EXTRACTIONVO)
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
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>
     
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v
deleted file mode 100644
index 011bc81e5..000000000
--- a/plugins/field/LegacyField.v
+++ /dev/null
@@ -1,14 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export LegacyField_Compl.
-Require Export LegacyField_Theory.
-Require Export LegacyField_Tactic.
-Declare ML Module "field_plugin".
-
-(* Command declarations are moved to the ML side *)
diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
deleted file mode 100644
index 97c70c0ec..000000000
--- a/plugins/field/LegacyField_Compl.v
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import List.
-
-Definition assoc_2nd :=
-  (fix assoc_2nd_rec (A:Type) (B:Set)
-                     (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
-                     (lst:list (prod A B)) {struct lst} :
-   B -> A -> A :=
-     fun (key:B) (default:A) =>
-       match lst with
-       | nil => default
-       | (v,e) :: l =>
-           match eq_dec e key with
-           | left _ => v
-           | right _ => assoc_2nd_rec A B eq_dec l key default
-           end
-       end).
-
-Definition mem :=
-  (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2})
-           (a:A) (l:list A) {struct l} : bool :=
-     match l with
-     | nil => false
-     | a1 :: l1 =>
-         match eq_dec a a1 with
-         | left _ => true
-         | right _ => mem A eq_dec a l1
-         end
-     end).
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
deleted file mode 100644
index 0a8d27ca3..000000000
--- a/plugins/field/LegacyField_Tactic.v
+++ /dev/null
@@ -1,431 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import List.
-Require Import LegacyRing.
-Require Export LegacyField_Compl.
-Require Export LegacyField_Theory.
-
-(**** Interpretation A --> ExprA ****)
-
-Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
-
-Ltac body_of s := eval cbv beta iota delta [s] in s.
-
-Ltac mem_assoc var lvar :=
-  match constr:lvar with
-  | nil => constr:false
-  | ?X1 :: ?X2 =>
-      match constr:(X1 = var) with
-      | (?X1 = ?X1) => constr:true
-      | _ => mem_assoc var X2
-      end
-  end.
-
-Ltac number lvar :=
-  let rec number_aux lvar cpt :=
-    match constr:lvar with
-    | (@nil ?X1) => constr:(@nil (prod X1 nat))
-    | ?X2 :: ?X3 =>
-        let l2 := number_aux X3 (S cpt) in
-        constr:((X2,cpt) :: l2)
-    end
-  in number_aux lvar 0.
-
-Ltac build_varlist FT trm :=
-  let rec seek_var lvar trm :=
-    let AT := get_component A FT
-    with AzeroT := get_component Azero FT
-    with AoneT := get_component Aone FT
-    with AplusT := get_component Aplus FT
-    with AmultT := get_component Amult FT
-    with AoppT := get_component Aopp FT
-    with AinvT := get_component Ainv FT in
-    match constr:trm with
-    | AzeroT => lvar
-    | AoneT => lvar
-    | (AplusT ?X1 ?X2) =>
-        let l1 := seek_var lvar X1 in
-        seek_var l1 X2
-    | (AmultT ?X1 ?X2) =>
-        let l1 := seek_var lvar X1 in
-        seek_var l1 X2
-    | (AoppT ?X1) => seek_var lvar X1
-    | (AinvT ?X1) => seek_var lvar X1
-    | ?X1 =>
-        let res := mem_assoc X1 lvar in
-        match constr:res with
-        | true => lvar
-        | false => constr:(X1 :: lvar)
-        end
-    end in
-  let AT := get_component A FT in
-  let lvar := seek_var (@nil AT) trm in
-  number lvar.
-
-Ltac assoc elt lst :=
-  match constr:lst with
-  | nil => fail
-  | (?X1,?X2) :: ?X3 =>
-      match constr:(elt = X1) with
-      | (?X1 = ?X1) => constr:X2
-      | _ => assoc elt X3
-      end
-  end.
-
-Ltac interp_A FT lvar trm :=
-  let AT := get_component A FT
-  with AzeroT := get_component Azero FT
-  with AoneT := get_component Aone FT
-  with AplusT := get_component Aplus FT
-  with AmultT := get_component Amult FT
-  with AoppT := get_component Aopp FT
-  with AinvT := get_component Ainv FT in
-  match constr:trm with
-  | AzeroT => constr:EAzero
-  | AoneT => constr:EAone
-  | (AplusT ?X1 ?X2) =>
-      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
-      constr:(EAplus e1 e2)
-  | (AmultT ?X1 ?X2) =>
-      let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
-      constr:(EAmult e1 e2)
-  | (AoppT ?X1) =>
-      let e := interp_A FT lvar X1 in
-      constr:(EAopp e)
-  | (AinvT ?X1) => let e := interp_A FT lvar X1 in
-                   constr:(EAinv e)
-  | ?X1 => let idx := assoc X1 lvar in
-           constr:(EAvar idx)
-  end.
-
-(************************)
-(*    Simplification    *)
-(************************)
-
-(**** Generation of the multiplier ****)
-
-Ltac remove e l :=
-  match constr:l with
-  | nil => l
-  | e :: ?X2 => constr:X2
-  | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
-  end.
-
-Ltac union l1 l2 :=
-  match constr:l1 with
-  | nil => l2
-  | ?X2 :: ?X3 =>
-      let nl2 := remove X2 l2 in
-      let nl := union X3 nl2 in
-      constr:(X2 :: nl)
-  end.
-
-Ltac raw_give_mult trm :=
-  match constr:trm with
-  | (EAinv ?X1) => constr:(X1 :: nil)
-  | (EAopp ?X1) => raw_give_mult X1
-  | (EAplus ?X1 ?X2) =>
-      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
-      union l1 l2
-  | (EAmult ?X1 ?X2) =>
-      let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
-      eval compute in (app l1 l2)
-  | _ => constr:(@nil ExprA)
-  end.
-
-Ltac give_mult trm :=
-  let ltrm := raw_give_mult trm in
-  constr:(mult_of_list ltrm).
-
-(**** Associativity ****)
-
-Ltac apply_assoc FT lvar trm :=
-  let t := eval compute in (assoc trm) in
-  match constr:(t = trm) with
-  | (?X1 = ?X1) => idtac
-  | _ =>
-      rewrite <- (assoc_correct FT trm); change (assoc trm) with t
-  end.
-
-(**** Distribution *****)
-
-Ltac apply_distrib FT lvar trm :=
-  let t := eval compute in (distrib trm) in
-  match constr:(t = trm) with
-  | (?X1 = ?X1) => idtac
-  | _ =>
-      rewrite <- (distrib_correct FT trm);
-       change (distrib trm) with t
-  end.
-
-(**** Multiplication by the inverse product ****)
-
-Ltac grep_mult := match goal with
-                  | id:(interp_ExprA _ _ _ <> _) |- _ => id
-                  end.
-
-Ltac weak_reduce :=
-  match goal with
-  |  |- context [(interp_ExprA ?X1 ?X2 _)] =>
-      cbv beta iota zeta
-       delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
-             Aone Aplus Amult Aopp Ainv]
-  end.
-
-Ltac multiply mul :=
-  match goal with
-  |  |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
-      let AzeroT := get_component Azero FT in
-      cut (interp_ExprA FT X2 mul <> AzeroT);
-       [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
-       | weak_reduce;
-          (let AoneT := get_component Aone ltac:(body_of FT)
-           with AmultT := get_component Amult ltac:(body_of FT) in
-           try
-             match goal with
-             |  |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
-             end; clear FT X2) ]
-  end.
-
-Ltac apply_multiply FT lvar trm :=
-  let t := eval compute in (multiply trm) in
-  match constr:(t = trm) with
-  | (?X1 = ?X1) => idtac
-  | _ =>
-      rewrite <- (multiply_correct FT trm);
-       change (multiply trm) with t
-  end.
-
-(**** Permutations and simplification ****)
-
-Ltac apply_inverse mul FT lvar trm :=
-  let t := eval compute in (inverse_simplif mul trm) in
-  match constr:(t = trm) with
-  | (?X1 = ?X1) => idtac
-  | _ =>
-      rewrite <- (inverse_correct FT trm mul);
-       [ change (inverse_simplif mul trm) with t | assumption ]
-  end.
-(**** Inverse test ****)
-
-Ltac strong_fail tac := first [ tac | fail 2 ].
-
-Ltac inverse_test_aux FT trm :=
-  let AplusT := get_component Aplus FT
-  with AmultT := get_component Amult FT
-  with AoppT := get_component Aopp FT
-  with AinvT := get_component Ainv FT in
-  match constr:trm with
-  | (AinvT _) => fail 1
-  | (AoppT ?X1) =>
-      strong_fail ltac:(inverse_test_aux FT X1; idtac)
-  | (AplusT ?X1 ?X2) =>
-      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
-  | (AmultT ?X1 ?X2) =>
-      strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
-  | _ => idtac
-  end.
-
-Ltac inverse_test FT :=
-  let AplusT := get_component Aplus FT in
-  match goal with
-  |  |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
-  end.
-
-(**** Field itself ****)
-
-Ltac apply_simplif sfun :=
-  match goal with
-  |  |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) =>
-  sfun X1 X2 X3
-  end;
-   match goal with
-   |  |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) =>
-   sfun X1 X2 X3
-   end.
-
-Ltac unfolds FT :=
-  match get_component Aminus FT with
-  | Some ?X1 => unfold X1
-  | _ => idtac
-  end;
-  match get_component Adiv FT with
-  | Some ?X1 => unfold X1
-  | _ => idtac
-  end.
-
-Ltac reduce FT :=
-  let AzeroT := get_component Azero FT
-  with AoneT := get_component Aone FT
-  with AplusT := get_component Aplus FT
-  with AmultT := get_component Amult FT
-  with AoppT := get_component Aopp FT
-  with AinvT := get_component Ainv FT in
-  (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] ||
-     compute).
-
-Ltac field_gen_aux FT :=
-  let AplusT := get_component Aplus FT in
-  match goal with
-  |  |- (?X1 = ?X2) =>
-      let lvar := build_varlist FT (AplusT X1 X2) in
-      let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
-      let mul := give_mult (EAplus trm1 trm2) in
-      cut
-        (let ft := FT in
-         let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
-        [ compute; auto
-        | intros ft vm; apply_simplif apply_distrib;
-           apply_simplif apply_assoc; multiply mul;
-           [ apply_simplif apply_multiply;
-              apply_simplif ltac:(apply_inverse mul);
-              (let id := grep_mult in
-               clear id; weak_reduce; clear ft vm; first
-              [ inverse_test FT; legacy ring | field_gen_aux FT ])
-           | idtac ] ]
-  end.
-
-Ltac field_gen FT :=
-  unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
-
-(*****************************)
-(*    Term Simplification    *)
-(*****************************)
-
-(**** Minus and division expansions ****)
-
-Ltac init_exp FT trm :=
-  let e :=
-   (match get_component Aminus FT with
-    | Some ?X1 => eval cbv beta delta [X1] in trm
-    | _ => trm
-    end) in
-  match get_component Adiv FT with
-  | Some ?X1 => eval cbv beta delta [X1] in e
-  | _ => e
-  end.
-
-(**** Inverses simplification ****)
-
-Ltac simpl_inv trm :=
-  match constr:trm with
-  | (EAplus ?X1 ?X2) =>
-      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
-      constr:(EAplus e1 e2)
-  | (EAmult ?X1 ?X2) =>
-      let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
-      constr:(EAmult e1 e2)
-  | (EAopp ?X1) => let e := simpl_inv X1 in
-                   constr:(EAopp e)
-  | (EAinv ?X1) => SimplInvAux X1
-  | ?X1 => constr:X1
-  end
- with SimplInvAux trm :=
-  match constr:trm with
-  | (EAinv ?X1) => simpl_inv X1
-  | (EAmult ?X1 ?X2) =>
-      let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
-      constr:(EAmult e1 e2)
-  | ?X1 => let e := simpl_inv X1 in
-           constr:(EAinv e)
-  end.
-
-(**** Monom simplification ****)
-
-Ltac map_tactic fcn lst :=
-  match constr:lst with
-  | nil => lst
-  | ?X2 :: ?X3 =>
-      let r := fcn X2 with t := map_tactic fcn X3 in
-      constr:(r :: t)
-  end.
-
-Ltac build_monom_aux lst trm :=
-  match constr:lst with
-  | nil => eval compute in (assoc trm)
-  | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
-  end.
-
-Ltac build_monom lnum lden :=
-  let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
-  let ltot := eval compute in (app lnum ildn) in
-  let trm := build_monom_aux ltot EAone in
-  match constr:trm with
-  | (EAmult _ ?X1) => constr:X1
-  | ?X1 => constr:X1
-  end.
-
-Ltac simpl_monom_aux lnum lden trm :=
-  match constr:trm with
-  | (EAmult (EAinv ?X1) ?X2) =>
-      let mma := mem_assoc X1 lnum in
-      match constr:mma with
-      | true =>
-          let newlnum := remove X1 lnum in
-          simpl_monom_aux newlnum lden X2
-      | false => simpl_monom_aux lnum (X1 :: lden) X2
-      end
-  | (EAmult ?X1 ?X2) =>
-      let mma := mem_assoc X1 lden in
-      match constr:mma with
-      | true =>
-          let newlden := remove X1 lden in
-          simpl_monom_aux lnum newlden X2
-      | false => simpl_monom_aux (X1 :: lnum) lden X2
-      end
-  | (EAinv ?X1) =>
-      let mma := mem_assoc X1 lnum in
-      match constr:mma with
-      | true =>
-          let newlnum := remove X1 lnum in
-          build_monom newlnum lden
-      | false => build_monom lnum (X1 :: lden)
-      end
-  | ?X1 =>
-      let mma := mem_assoc X1 lden in
-      match constr:mma with
-      | true =>
-          let newlden := remove X1 lden in
-          build_monom lnum newlden
-      | false => build_monom (X1 :: lnum) lden
-      end
-  end.
-
-Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
-
-Ltac simpl_all_monomials trm :=
-  match constr:trm with
-  | (EAplus ?X1 ?X2) =>
-      let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
-      constr:(EAplus e1 e2)
-  | ?X1 => simpl_monom X1
-  end.
-
-(**** Associativity and distribution ****)
-
-Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
-
-(**** The tactic Field_Term ****)
-
-Ltac eval_weak_reduce trm :=
-  eval
-   cbv beta iota zeta
-    delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
-          Amult Aopp Ainv] in trm.
-
-Ltac field_term FT exp :=
-  let newexp := init_exp FT exp in
-  let lvar := build_varlist FT newexp in
-  let trm := interp_A FT lvar newexp in
-  let tma := eval compute in (assoc trm) in
-  let tsmp :=
-   simpl_all_monomials
-    ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
-  let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
-  (replace exp with trep; [ legacy ring trep | field_gen FT ]).
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
deleted file mode 100644
index ac66e6d35..000000000
--- a/plugins/field/LegacyField_Theory.v
+++ /dev/null
@@ -1,648 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import List.
-Require Import Peano_dec.
-Require Import LegacyRing.
-Require Import LegacyField_Compl.
-
-Record Field_Theory : Type :=
-  {A : Type;
-   Aplus : A -> A -> A;
-   Amult : A -> A -> A;
-   Aone : A;
-   Azero : A;
-   Aopp : A -> A;
-   Aeq : A -> A -> bool;
-   Ainv : A -> A;
-   Aminus : option (A -> A -> A);
-   Adiv : option (A -> A -> A);
-   RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
-   Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
-
-(* The reflexion structure *)
-Inductive ExprA : Set :=
-  | EAzero : ExprA
-  | EAone : ExprA
-  | EAplus : ExprA -> ExprA -> ExprA
-  | EAmult : ExprA -> ExprA -> ExprA
-  | EAopp : ExprA -> ExprA
-  | EAinv : ExprA -> ExprA
-  | EAvar : nat -> ExprA.
-
-(**** Decidability of equality ****)
-
-Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}.
-Proof.
-  double induction e1 e2; try intros;
-   try (left; reflexivity) || (try (right; discriminate)).
-  elim (H1 e0); intro y; elim (H2 e); intro y0;
-   try
-    (left; rewrite y; rewrite y0; auto) ||
-      (right; red; intro; inversion H3; auto).
-  elim (H1 e0); intro y; elim (H2 e); intro y0;
-   try
-    (left; rewrite y; rewrite y0; auto) ||
-      (right; red; intro; inversion H3; auto).
-  elim (H0 e); intro y.
-  left; rewrite y; auto.
-  right; red; intro; inversion H1; auto.
-  elim (H0 e); intro y.
-  left; rewrite y; auto.
-  right; red; intro; inversion H1; auto.
-  elim (eq_nat_dec n n0); intro y.
-  left; rewrite y; auto.
-  right; red; intro; inversion H; auto.
-Defined.
-
-Definition eq_nat_dec := Eval compute in eq_nat_dec.
-Definition eqExprA := Eval compute in eqExprA_O.
-
-(**** Generation of the multiplier ****)
-
-Fixpoint mult_of_list (e:list ExprA) : ExprA :=
-  match e with
-  | nil => EAone
-  | e1 :: l1 => EAmult e1 (mult_of_list l1)
-  end.
-
-Section Theory_of_fields.
-
-Variable T : Field_Theory.
-
-Let AT := A T.
-Let AplusT := Aplus T.
-Let AmultT := Amult T.
-Let AoneT := Aone T.
-Let AzeroT := Azero T.
-Let AoppT := Aopp T.
-Let AeqT := Aeq T.
-Let AinvT := Ainv T.
-Let RTT := RT T.
-Let Th_inv_defT := Th_inv_def T.
-
-Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
- Azero T) (Aopp T) (Aeq T) (RT T).
-
-Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
-
-(***************************)
-(*    Lemmas to be used    *)
-(***************************)
-
-Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AplusT_assoc :
- forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AmultT_assoc :
- forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma AmultT_AplusT_distr :
- forall r1 r2 r3:AT,
-   AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
-Proof.
-  intros; legacy ring.
-Qed.
-
-Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.
-Proof.
-  intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
-  legacy ring.
-  transitivity (AplusT (AplusT (AoppT r) r) r2).
-  repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
-  legacy ring.
-Qed.
-
-Lemma r_AmultT_mult :
- forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2.
-Proof.
-  intros; transitivity (AmultT (AmultT (AinvT r) r) r1).
-  rewrite Th_inv_defT; [ symmetry ; apply AmultT_1l; auto | auto ].
-  transitivity (AmultT (AmultT (AinvT r) r) r2).
-  repeat rewrite AmultT_assoc; rewrite H; trivial.
-  rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ].
-Qed.
-
-Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
-Proof.
-  intro; legacy ring.
-Qed.
-
-Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
-Proof.
-  intro; legacy ring.
-Qed.
-
-Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
-Proof.
-  intro; legacy ring.
-Qed.
-
-Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
-Proof.
-  intros; rewrite AmultT_comm; apply Th_inv_defT; auto.
-Qed.
-
-Lemma Rmult_neq_0_reg :
- forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
-Proof.
-  intros r1 r2 H; split; red; intro; apply H; rewrite H0; legacy ring.
-Qed.
-
-(************************)
-(*    Interpretation    *)
-(************************)
-
-(**** ExprA --> A ****)
-
-Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
- AT :=
-  match e with
-  | EAzero => AzeroT
-  | EAone => AoneT
-  | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
-  | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
-  | EAopp e => Aopp T (interp_ExprA lvar e)
-  | EAinv e => Ainv T (interp_ExprA lvar e)
-  | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT
-  end.
-
-(************************)
-(*    Simplification    *)
-(************************)
-
-(**** Associativity ****)
-
-Definition merge_mult :=
-  (fix merge_mult (e1:ExprA) : ExprA -> ExprA :=
-     fun e2:ExprA =>
-       match e1 with
-       | EAmult t1 t2 =>
-           match t2 with
-           | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2))
-           | _ => EAmult t1 (EAmult t2 e2)
-           end
-       | _ => EAmult e1 e2
-       end).
-
-Fixpoint assoc_mult (e:ExprA) : ExprA :=
-  match e with
-  | EAmult e1 e3 =>
-      match e1 with
-      | EAmult e1 e2 =>
-          merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
-            (assoc_mult e3)
-      | _ => EAmult e1 (assoc_mult e3)
-      end
-  | _ => e
-  end.
-
-Definition merge_plus :=
-  (fix merge_plus (e1:ExprA) : ExprA -> ExprA :=
-     fun e2:ExprA =>
-       match e1 with
-       | EAplus t1 t2 =>
-           match t2 with
-           | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2))
-           | _ => EAplus t1 (EAplus t2 e2)
-           end
-       | _ => EAplus e1 e2
-       end).
-
-Fixpoint assoc (e:ExprA) : ExprA :=
-  match e with
-  | EAplus e1 e3 =>
-      match e1 with
-      | EAplus e1 e2 =>
-          merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3)
-      | _ => EAplus (assoc_mult e1) (assoc e3)
-      end
-  | _ => assoc_mult e
-  end.
-
-Lemma merge_mult_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
-   interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).
-Proof.
-intros e1 e2; generalize e1; generalize e2; clear e1 e2.
-simple induction e2; auto; intros.
-unfold merge_mult at 1; fold merge_mult;
- unfold interp_ExprA at 2; fold interp_ExprA;
- rewrite (H0 e e3 lvar); unfold interp_ExprA at 1;
- fold interp_ExprA; unfold interp_ExprA at 5;
- fold interp_ExprA; auto.
-Qed.
-
-Lemma merge_mult_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
-Proof.
-simple induction e1; auto; intros.
-elim e0; try (intros; simpl; legacy ring).
-unfold interp_ExprA in H2; fold interp_ExprA in H2;
- cut
-  (AmultT (interp_ExprA lvar e2)
-     (AmultT (interp_ExprA lvar e4)
-        (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
-   AmultT
-     (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4))
-        (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
-intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1;
- simpl; legacy ring.
-legacy ring.
-Qed.
-
-Lemma assoc_mult_correct1 :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   AmultT (interp_ExprA lvar (assoc_mult e1))
-     (interp_ExprA lvar (assoc_mult e2)) =
-   interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
-Proof.
-simple induction e1; auto; intros.
-rewrite <- (H e0 lvar); simpl; rewrite merge_mult_correct;
- simpl; rewrite merge_mult_correct; simpl;
- auto.
-Qed.
-
-Lemma assoc_mult_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
-Proof.
-simple induction e; auto; intros.
-elim e0; intros.
-intros; simpl; legacy ring.
-simpl; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
- rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite merge_mult_correct; simpl;
- rewrite merge_mult_correct; simpl; rewrite AmultT_assoc;
- rewrite assoc_mult_correct1; rewrite H2; simpl;
- rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1;
- fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
- rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
- rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc;
- legacy ring.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-Qed.
-
-Lemma merge_plus_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
-   interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).
-Proof.
-intros e1 e2; generalize e1; generalize e2; clear e1 e2.
-simple induction e2; auto; intros.
-unfold merge_plus at 1; fold merge_plus;
- unfold interp_ExprA at 2; fold interp_ExprA;
- rewrite (H0 e e3 lvar); unfold interp_ExprA at 1;
- fold interp_ExprA; unfold interp_ExprA at 5;
- fold interp_ExprA; auto.
-Qed.
-
-Lemma merge_plus_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
-Proof.
-simple induction e1; auto; intros.
-elim e0; try intros; try (simpl; legacy ring).
-unfold interp_ExprA in H2; fold interp_ExprA in H2;
- cut
-  (AplusT (interp_ExprA lvar e2)
-     (AplusT (interp_ExprA lvar e4)
-        (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
-   AplusT
-     (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4))
-        (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
-intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1;
- simpl; legacy ring.
-legacy ring.
-Qed.
-
-Lemma assoc_plus_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
-   interp_ExprA lvar (assoc (EAplus e1 e2)).
-Proof.
-simple induction e1; auto; intros.
-rewrite <- (H e0 lvar); simpl; rewrite merge_plus_correct;
- simpl; rewrite merge_plus_correct; simpl;
- auto.
-Qed.
-
-Lemma assoc_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
-Proof.
-simple induction e; auto; intros.
-elim e0; intros.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite merge_plus_correct; simpl;
- rewrite merge_plus_correct; simpl; rewrite AplusT_assoc;
- rewrite assoc_plus_correct; rewrite H2; simpl;
- apply
-  (r_AplusT_plus (interp_ExprA lvar (assoc e1))
-     (AplusT (interp_ExprA lvar (assoc e2))
-        (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1)))
-     (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3))
-        (interp_ExprA lvar e1))); rewrite <- AplusT_assoc;
- rewrite
-  (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
-  ; rewrite assoc_plus_correct; rewrite H1; simpl;
- rewrite (H0 lvar);
- rewrite <-
-  (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1))
-     (interp_ExprA lvar e3) (interp_ExprA lvar e1))
-  ;
- rewrite
-  (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1)
-     (interp_ExprA lvar e3));
- rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3));
- rewrite <-
-  (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
-     (interp_ExprA lvar e1)); apply AplusT_comm.
-unfold assoc; fold assoc; unfold interp_ExprA;
- fold interp_ExprA; rewrite assoc_mult_correct;
- rewrite (H0 lvar); simpl; auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-unfold assoc; fold assoc; unfold interp_ExprA;
- fold interp_ExprA; rewrite assoc_mult_correct;
- simpl; auto.
-Qed.
-
-(**** Distribution *****)
-
-Fixpoint distrib_EAopp (e:ExprA) : ExprA :=
-  match e with
-  | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2)
-  | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2)
-  | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e)
-  | e => e
-  end.
-
-Definition distrib_mult_right :=
-  (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA :=
-     fun e2:ExprA =>
-       match e1 with
-       | EAplus t1 t2 =>
-           EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)
-       | _ => EAmult e1 e2
-       end).
-
-Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA :=
-  match e1 with
-  | EAplus t1 t2 =>
-      EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2)
-  | _ => distrib_mult_right e2 e1
-  end.
-
-Fixpoint distrib_main (e:ExprA) : ExprA :=
-  match e with
-  | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2)
-  | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2)
-  | EAopp e => EAopp (distrib_main e)
-  | _ => e
-  end.
-
-Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
-
-Lemma distrib_mult_right_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (distrib_mult_right e1 e2) =
-   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
-Proof.
-simple induction e1; try intros; simpl; auto.
-rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
- rewrite (H0 e2 lvar); legacy ring.
-Qed.
-
-Lemma distrib_mult_left_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (distrib_mult_left e1 e2) =
-   AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
-Proof.
-simple induction e1; try intros; simpl.
-rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl;
- apply AmultT_Or.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite AmultT_comm;
- rewrite
-  (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
-     (interp_ExprA lvar e0));
- rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e));
- rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0));
- rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-Qed.
-
-Lemma distrib_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; rewrite <- (H lvar); rewrite <- (H0 lvar);
- unfold distrib; simpl; auto.
-simpl; rewrite <- (H lvar); rewrite <- (H0 lvar);
- unfold distrib; simpl; apply distrib_mult_left_correct.
-simpl; fold AoppT; rewrite <- (H lvar);
- unfold distrib; simpl; rewrite distrib_mult_right_correct;
- simpl; fold AoppT; legacy ring.
-Qed.
-
-(**** Multiplication by the inverse product ****)
-
-Lemma mult_eq :
- forall (e1 e2 a:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar a <> AzeroT ->
-   interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) ->
-   interp_ExprA lvar e1 = interp_ExprA lvar e2.
-Proof.
-  simpl; intros;
-   apply
-    (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
-       (interp_ExprA lvar e2)); assumption.
-Qed.
-
-Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA :=
-  match e with
-  | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2)
-  | _ => EAmult a e
-  end.
-
-Definition multiply (e:ExprA) : ExprA :=
-  match e with
-  | EAmult a e1 => multiply_aux a e1
-  | _ => e
-  end.
-
-Lemma multiply_aux_correct :
- forall (a e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (multiply_aux a e) =
-   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction e; simpl; intros; try rewrite merge_mult_correct;
- auto.
-  simpl; rewrite (H0 lvar); legacy ring.
-Qed.
-
-Lemma multiply_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
-Proof.
-  simple induction e; simpl; auto.
-  intros; apply multiply_aux_correct.
-Qed.
-
-(**** Permutations and simplification ****)
-
-Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA :=
-  match m with
-  | EAmult m0 m1 =>
-      match eqExprA m0 (EAinv a) with
-      | left _ => m1
-      | right _ => EAmult m0 (monom_remove a m1)
-      end
-  | _ =>
-      match eqExprA m (EAinv a) with
-      | left _ => EAone
-      | right _ => EAmult a m
-      end
-  end.
-
-Definition monom_simplif_rem :=
-  (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA :=
-     fun m:ExprA =>
-       match a with
-       | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m)
-       | _ => monom_remove a m
-       end).
-
-Definition monom_simplif (a m:ExprA) : ExprA :=
-  match m with
-  | EAmult a' m' =>
-      match eqExprA a a' with
-      | left _ => monom_simplif_rem a m'
-      | right _ => m
-      end
-  | _ => m
-  end.
-
-Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
-  match e with
-  | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2)
-  | _ => monom_simplif a e
-  end.
-
-Lemma monom_remove_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar a <> AzeroT ->
-   interp_ExprA lvar (monom_remove a e) =
-   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction e; intros.
-simpl; case (eqExprA EAzero (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-simpl; case (eqExprA EAone (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-simpl; case (eqExprA (EAplus e0 e1) (EAinv a)); intros;
- [ inversion e2 | simpl; trivial ].
-simpl; case (eqExprA e0 (EAinv a)); intros.
-rewrite e2; simpl; fold AinvT.
-rewrite <-
- (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
-    (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ].
-simpl; rewrite H0; auto; legacy ring.
-simpl; fold AoppT; case (eqExprA (EAopp e0) (EAinv a));
- intros; [ inversion e1 | simpl; trivial ].
-unfold monom_remove; case (eqExprA (EAinv e0) (EAinv a)); intros.
-case (eqExprA e0 a); intros.
-rewrite e2; simpl; fold AinvT; rewrite AinvT_r; auto.
-inversion e1; simpl; exfalso; auto.
-simpl; trivial.
-unfold monom_remove; case (eqExprA (EAvar n) (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-Qed.
-
-Lemma monom_simplif_rem_correct :
- forall (a e:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar a <> AzeroT ->
-   interp_ExprA lvar (monom_simplif_rem a e) =
-   AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction a; simpl; intros; try rewrite monom_remove_correct;
- auto.
-elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1);
- intros.
-rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto.
-legacy ring.
-Qed.
-
-Lemma monom_simplif_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar a <> AzeroT ->
-   interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; case (eqExprA a e0); intros.
-rewrite <- e2; apply monom_simplif_rem_correct; auto.
-simpl; trivial.
-Qed.
-
-Lemma inverse_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
-   interp_ExprA lvar a <> AzeroT ->
-   interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
-unfold inverse_simplif; rewrite monom_simplif_correct; auto.
-Qed.
-
-End Theory_of_fields.
-
-(* Compatibility *)
-Notation AplusT_sym := AplusT_comm (only parsing).
-Notation AmultT_sym := AmultT_comm (only parsing).
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
deleted file mode 100644
index 988e56af5..000000000
--- a/plugins/field/field.ml4
+++ /dev/null
@@ -1,192 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Names
-open Pp
-open Proof_type
-open Tacinterp
-open Tacmach
-open Term
-open Typing
-open Errors
-open Util
-open Vernacinterp
-open Vernacexpr
-open Tacexpr
-open Mod_subst
-open Coqlib
-
-(* Interpretation of constr's *)
-let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
-
-(* Construction of constants *)
-let constant dir s = gen_constant "Field" ("field"::dir) s
-let init_constant s = gen_constant_in_modules "Field" init_modules s
-
-(* To deal with the optional arguments *)
-let constr_of_opt a opt =
-  let ac = constr_of a in
-  let ac3 = mkArrow ac (mkArrow ac ac) in
-  match opt with
-  | None -> mkApp (init_constant "None",[|ac3|])
-  | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
-
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
-
-(* Table of theories *)
-let th_tab = ref (Cmap.empty : constr Cmap.t)
-
-let lookup env typ =
-  try Cmap.find typ !th_tab
-  with Not_found ->
-    errorlabstrm "field"
-      (str "No field is declared for type" ++ spc() ++
-      Printer.pr_lconstr_env env typ)
-
-let _ =
-  let init () = th_tab := Cmap.empty in
-  let freeze () = !th_tab in
-  let unfreeze fs = th_tab := fs in
-  Summary.declare_summary "field"
-    { Summary.freeze_function   = freeze;
-      Summary.unfreeze_function = unfreeze;
-      Summary.init_function     = init }
-
-let load_addfield _ = ()
-let cache_addfield (_,(typ,th)) = th_tab := Cmap.add typ th !th_tab
-let subst_addfield (subst,(typ,th as obj)) =
-  let typ' = subst_mps subst typ in
-  let th' = subst_mps subst th in
-    if typ' == typ && th' == th then obj else
-      (typ',th')
-
-(* Declaration of the Add Field library object *)
-let in_addfield : types * constr -> Libobject.obj =
-  Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
-       Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
-       Libobject.cache_function = cache_addfield;
-       Libobject.subst_function = subst_addfield;
-       Libobject.classify_function = (fun a -> Libobject.Substitute a)}
-
-(* Adds a theory to the table *)
-let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
-  ainv_l =
-  begin
-    (try
-      Ring.add_theory true true false a None None None aplus amult aone azero
-        (Some aopp) aeq rth Quote.ConstrSet.empty
-     with | UserError("Add Semi Ring",_) -> ());
-    let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
-      [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
-    begin
-      let _ = type_of (Global.env ()) Evd.empty th in ();
-      Lib.add_anonymous_leaf (in_addfield (a,th))
-    end
-  end
-
-(* Vernac command declaration *)
-open Extend
-open Pcoq
-open Genarg
-
-VERNAC ARGUMENT EXTEND divarg
-| [ "div" ":=" constr(adiv) ] -> [ adiv ]
-END
-
-VERNAC ARGUMENT EXTEND minusarg
-| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
-END
-
-(*
-(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
-VERNAC ARGUMENT EXTEND minus_div_arg
-| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
-| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
-| [ ] -> [ None, None ]
-END
-*)
-
-(* For the translator, otherwise the code above is OK *)
-open Ppconstr
-let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
-  if omin=None && odiv=None then mt() else
-    spc() ++ str "with" ++
-    pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
-    pr_opt (fun c -> str "div := " ++ _prc c) odiv
-(*
-let () =
-  Pptactic.declare_extra_genarg_pprule true
-    (rawwit_minus_div_arg,pp_minus_div_arg)
-    (globwit_minus_div_arg,pp_minus_div_arg)
-    (wit_minus_div_arg,pp_minus_div_arg)
-*)
-ARGUMENT EXTEND minus_div_arg
-  TYPED AS constr_opt * constr_opt
-  PRINTED BY pp_minus_div_arg
-| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
-| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
-| [ ] -> [ None, None ]
-END
-
-VERNAC COMMAND EXTEND Field
-  [ "Add" "Legacy" "Field"
-      constr(a) constr(aplus) constr(amult) constr(aone)
-      constr(azero) constr(aopp) constr(aeq)
-      constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
-    -> [ let (aminus_o, adiv_o) = md in
-         add_field
-           (constr_of a) (constr_of aplus) (constr_of amult)
-           (constr_of aone) (constr_of azero) (constr_of aopp)
-           (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
-           (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
-END
-
-(* Guesses the type and calls field_gen with the right theory *)
-let field g =
-  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
-  let typ =
-    try match Hipattern.match_with_equation (pf_concl g) with
-      | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
-      | _ -> raise Exit
-    with Hipattern.NoEquationFound | Exit ->
-      error "The statement is not built from Leibniz' equality" in
-  let th = VConstr ([],lookup (pf_env g) typ) in
-  (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
-    <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
-
-(* Verifies that all the terms have the same type and gives the right theory *)
-let guess_theory env evc = function
-  | c::tl ->
-    let t = type_of env evc c in
-    if List.exists (fun c1 ->
-      not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then
-      errorlabstrm "Field:" (str" All the terms must have the same type")
-    else
-      lookup env t
-  | [] -> anomaly "Field: must have a non-empty constr list here"
-
-(* Guesses the type and calls Field_Term with the right theory *)
-let field_term l g =
-  Coqlib.check_required_library ["Coq";"field";"LegacyField"];
-  let env = (pf_env g)
-  and evc = (project g) in
-  let th = valueIn (VConstr ([],guess_theory env evc l))
-  and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
-  (List.fold_right
-    (fun c a ->
-     let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
-     Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
-
-(* Declaration of Field *)
-
-TACTIC EXTEND legacy_field
-| [ "legacy" "field" ] -> [ field ]
-| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
-END
diff --git a/plugins/field/field_plugin.mllib b/plugins/field/field_plugin.mllib
deleted file mode 100644
index 3c3e87af5..000000000
--- a/plugins/field/field_plugin.mllib
+++ /dev/null
@@ -1,2 +0,0 @@
-Field
-Field_plugin_mod
diff --git a/plugins/field/vo.itarget b/plugins/field/vo.itarget
deleted file mode 100644
index 22b56f330..000000000
--- a/plugins/field/vo.itarget
+++ /dev/null
@@ -1,4 +0,0 @@
-LegacyField_Compl.vo
-LegacyField_Tactic.vo
-LegacyField_Theory.vo
-LegacyField.vo
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index a1113d2d0..1e944a452 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -8,8 +8,7 @@
 
 (* "Fourier's method to solve linear inequations/equations systems.".*)
 
-Require Export LegacyRing.
-Require Export LegacyField.
+Require Export Field.
 Require Export DiscrR.
 Require Export Fourier_util.
 Declare ML Module "fourier_plugin".
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index c9760de17..a4dbb43c5 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -605,7 +605,7 @@ let rec fourier gl=
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
       			        [tclORELSE
-                                   (Ring.polynom [])
+                                   (* TODO : Ring.polynom []*) tclIDTAC
                                    tclIDTAC;
 					  (tclTHEN (apply (get coq_sym_eqT))
 						(apply (get coq_Rinv_1)))]
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 114ac0ab4..21c20280c 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -16,7 +16,6 @@ Require Import ZMicromega.
 Require Import QMicromega.
 Require Import RMicromega.
 Require Import QArith.
-Require Export Ring_normalize.
 Require Import ZArith.
 Require Import Rdefinitions.
 Require Export RingMicromega.
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 19af8d57e..c7249fe3a 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -17,7 +17,6 @@
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
 open Quote
-open Ring
 open Mutils
 open Glob_term
 open Errors
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index af8412cc7..8f68cc696 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -1,5 +1,4 @@
 btauto/btauto_plugin.cma
-field/field_plugin.cma
 setoid_ring/newring_plugin.cma
 extraction/extraction_plugin.cma
 decl_mode/decl_mode_plugin.cma
@@ -10,7 +9,6 @@ romega/romega_plugin.cma
 omega/omega_plugin.cma
 micromega/micromega_plugin.cma
 xml/xml_plugin.cma
-ring/ring_plugin.cma
 cc/cc_plugin.cma
 nsatz/nsatz_plugin.cma
 funind/recdef_plugin.cma
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 29737b9ce..01ac840dd 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -1,5 +1,4 @@
 btauto/btauto_plugin.cmxa
-field/field_plugin.cmxa
 setoid_ring/newring_plugin.cmxa
 extraction/extraction_plugin.cmxa
 decl_mode/decl_mode_plugin.cmxa
@@ -10,7 +9,6 @@ romega/romega_plugin.cmxa
 omega/omega_plugin.cmxa
 micromega/micromega_plugin.cmxa
 xml/xml_plugin.cmxa
-ring/ring_plugin.cmxa
 cc/cc_plugin.cmxa
 nsatz/nsatz_plugin.cmxa
 funind/recdef_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index ae2abeb41..4b698cccb 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -1,12 +1,10 @@
 btauto/vo.otarget
-field/vo.otarget
 fourier/vo.otarget
 funind/vo.otarget
 nsatz/vo.otarget
 micromega/vo.otarget
 omega/vo.otarget
 quote/vo.otarget
-ring/vo.otarget
 romega/vo.otarget
 rtauto/vo.otarget
 setoid_ring/vo.otarget
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
deleted file mode 100644
index 9c059cea1..000000000
--- a/plugins/ring/LegacyArithRing.v
+++ /dev/null
@@ -1,88 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the naturals of Arith $*)
-
-Require Import Bool.
-Require Export LegacyRing.
-Require Export Arith.
-Require Import Eqdep_dec.
-
-Local Open Scope nat_scope.
-
-Fixpoint nateq (n m:nat) {struct m} : bool :=
-  match n, m with
-  | O, O => true
-  | S n', S m' => nateq n' m'
-  | _, _ => false
-  end.
-
-Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m.
-Proof.
-  simple induction n; simple induction m; intros; try contradiction.
-  trivial.
-  unfold Is_true in H1.
-  rewrite (H n1 H1).
-  trivial.
-Qed.
-
-Hint Resolve nateq_prop: arithring.
-
-Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
-  split; intros; auto with arith arithring.
-(*  apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
-  trivial.*)
-Defined.
-
-
-Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
-
-Goal forall n:nat, S n = 1 + n.
-intro; reflexivity.
-Save S_to_plus_one.
-
-(* Replace all occurrences of (S exp) by (plus (S O) exp), except when
-   exp is already O and only for those occurrences than can be reached by going
-   down plus and mult operations  *)
-Ltac rewrite_S_to_plus_term t :=
-  match constr:t with
-  | 1 => constr:1
-  | (S ?X1) =>
-      let t1 := rewrite_S_to_plus_term X1 in
-      constr:(1 + t1)
-  | (?X1 + ?X2) =>
-      let t1 := rewrite_S_to_plus_term X1
-      with t2 := rewrite_S_to_plus_term X2 in
-      constr:(t1 + t2)
-  | (?X1 * ?X2) =>
-      let t1 := rewrite_S_to_plus_term X1
-      with t2 := rewrite_S_to_plus_term X2 in
-      constr:(t1 * t2)
-  | _ => constr:t
-  end.
-
-(* Apply S_to_plus on both sides of an equality *)
-Ltac rewrite_S_to_plus :=
-  match goal with
-  |  |- (?X1 = ?X2) =>
-      try
-       let t1 :=
-       (**)  (**)
-       rewrite_S_to_plus_term X1
-       with t2 := rewrite_S_to_plus_term X2 in
-       change (t1 = t2)
-  |  |- (?X1 = ?X2) =>
-      try
-       let t1 :=
-       (**)  (**)
-       rewrite_S_to_plus_term X1
-       with t2 := rewrite_S_to_plus_term X2 in
-       change (t1 = t2)
-  end.
-
-Ltac ring_nat := rewrite_S_to_plus; ring.
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
deleted file mode 100644
index a69cf0957..000000000
--- a/plugins/ring/LegacyNArithRing.v
+++ /dev/null
@@ -1,43 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the binary natural numbers *)
-
-Require Import Bool.
-Require Export LegacyRing.
-Require Export ZArith_base.
-Require Import NArith.
-Require Import Eqdep_dec.
-
-Definition Neq (n m:N) :=
-  match (n ?= m)%N with
-  | Datatypes.Eq => true
-  | _ => false
-  end.
-
-Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
-  intros n m H; unfold Neq in H.
-  apply N.compare_eq.
-  destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
-Qed.
-
-Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
-  split.
-    apply N.add_comm.
-    apply N.add_assoc.
-    apply N.mul_comm.
-    apply N.mul_assoc.
-    apply N.add_0_l.
-    apply N.mul_1_l.
-    apply N.mul_0_l.
-    apply N.mul_add_distr_r.
-    apply Neq_prop.
-Qed.
-
-Add Legacy Semi Ring
-  N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v
deleted file mode 100644
index 132014331..000000000
--- a/plugins/ring/LegacyRing.v
+++ /dev/null
@@ -1,35 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Bool.
-Require Export LegacyRing_theory.
-Require Export Quote.
-Require Export Ring_normalize.
-Require Export Ring_abstract.
-Declare ML Module "ring_plugin".
-
-(* As an example, we provide an instantation for bool. *)
-(* Other instatiations are given in ArithRing and ZArithRing in the
-   same directory *)
-
-Definition BoolTheory :
-  Ring_Theory xorb andb true false (fun b:bool => b) eqb.
-split; simpl.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct x; destruct y; reflexivity || simpl; tauto.
-Defined.
-
-Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ].
diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v
deleted file mode 100644
index d0bc46ea4..000000000
--- a/plugins/ring/LegacyRing_theory.v
+++ /dev/null
@@ -1,374 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Bool.
-
-Set Implicit Arguments.
-
-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.
-
-Infix "+" := Aplus (at level 50, left associativity).
-Infix "*" := Amult (at level 40, left associativity).
-Notation "0" := Azero.
-Notation "1" := Aone.
-
-Record Semi_Ring_Theory : Prop :=
-  {SR_plus_comm : forall n m:A, n + m = m + n;
-   SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
-   SR_mult_comm : forall n m:A, n * m = m * n;
-   SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
-   SR_plus_zero_left : forall n:A, 0 + n = n;
-   SR_mult_one_left : forall n:A, 1 * n = n;
-   SR_mult_zero_left : forall n:A, 0 * n = 0;
-   SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
-(*   SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*)
-   SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
-
-Variable T : Semi_Ring_Theory.
-
-Let plus_comm := SR_plus_comm T.
-Let plus_assoc := SR_plus_assoc T.
-Let mult_comm := SR_mult_comm T.
-Let mult_assoc := SR_mult_assoc T.
-Let plus_zero_left := SR_plus_zero_left T.
-Let mult_one_left := SR_mult_one_left T.
-Let mult_zero_left := SR_mult_zero_left T.
-Let distr_left := SR_distr_left T.
-(*Let plus_reg_left := SR_plus_reg_left T.*)
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left mult_zero_left distr_left (*plus_reg_left*).
-
-(* Lemmas whose form is x=y are also provided in form y=x because Auto does
-  not symmetry *)
-Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry ; eauto. Qed.
-
-Lemma SR_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry ; eauto. Qed.
-
-Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry ; eauto. Qed.
-
-Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
-intros.
-rewrite plus_assoc.
-elim (plus_comm m n).
-rewrite <- plus_assoc.
-reflexivity.
-Qed.
-
-Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
-intros.
-rewrite mult_assoc.
-elim (mult_comm m n).
-rewrite <- mult_assoc.
-reflexivity.
-Qed.
-
-Hint Resolve SR_plus_permute SR_mult_permute.
-
-Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
-intros.
-repeat rewrite (mult_comm n).
-eauto.
-Qed.
-
-Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry ; apply SR_distr_right. Qed.
-
-Lemma SR_mult_zero_right : forall n:A, n * 0 = 0.
-intro; rewrite mult_comm; eauto.
-Qed.
-
-Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0.
-intro; rewrite mult_comm; eauto.
-Qed.
-
-Lemma SR_plus_zero_right : forall n:A, n + 0 = n.
-intro; rewrite plus_comm; eauto.
-Qed.
-Lemma SR_plus_zero_right2 : forall n:A, n = n + 0.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma SR_mult_one_right : forall n:A, n * 1 = n.
-intro; elim mult_comm; auto.
-Qed.
-
-Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
-intro; elim mult_comm; auto.
-Qed.
-(*
-Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
-intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto.
-Qed.
-*)
-End Theory_of_semi_rings.
-
-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.
-
-Infix "+" := Aplus (at level 50, left associativity).
-Infix "*" := Amult (at level 40, left associativity).
-Notation "0" := Azero.
-Notation "1" := Aone.
-Notation "- x" := (Aopp x).
-
-Record Ring_Theory : Prop :=
-  {Th_plus_comm : forall n m:A, n + m = m + n;
-   Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
-   Th_mult_comm : forall n m:A, n * m = m * n;
-   Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
-   Th_plus_zero_left : forall n:A, 0 + n = n;
-   Th_mult_one_left : forall n:A, 1 * n = n;
-   Th_opp_def : forall n:A, n + - n = 0;
-   Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
-   Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
-
-Variable T : Ring_Theory.
-
-Let plus_comm := Th_plus_comm T.
-Let plus_assoc := Th_plus_assoc T.
-Let mult_comm := Th_mult_comm T.
-Let mult_assoc := Th_mult_assoc T.
-Let plus_zero_left := Th_plus_zero_left T.
-Let mult_one_left := Th_mult_one_left T.
-Let opp_def := Th_opp_def T.
-Let distr_left := Th_distr_left T.
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left opp_def distr_left.
-
-(* Lemmas whose form is x=y are also provided in form y=x because Auto does
-  not symmetry *)
-Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry ; eauto. Qed.
-
-Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry ; eauto. Qed.
-
-Lemma Th_opp_def2 : forall n:A, 0 = n + - n.
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
-intros.
-rewrite plus_assoc.
-elim (plus_comm m n).
-rewrite <- plus_assoc.
-reflexivity.
-Qed.
-
-Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
-intros.
-rewrite mult_assoc.
-elim (mult_comm m n).
-rewrite <- mult_assoc.
-reflexivity.
-Qed.
-
-Hint Resolve Th_plus_permute Th_mult_permute.
-
-Lemma aux1 : forall a:A, a + a = a -> a = 0.
-intros.
-generalize (opp_def a).
-pattern a at 1.
-rewrite <- H.
-rewrite <- plus_assoc.
-rewrite opp_def.
-elim plus_comm.
-rewrite plus_zero_left.
-trivial.
-Qed.
-
-Lemma Th_mult_zero_left : forall n:A, 0 * n = 0.
-intros.
-apply aux1.
-rewrite <- distr_left.
-rewrite plus_zero_left.
-reflexivity.
-Qed.
-Hint Resolve Th_mult_zero_left.
-
-Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry ; eauto. Qed.
-
-Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z.
-intros.
-rewrite <- (plus_zero_left y).
-elim H0.
-elim plus_assoc.
-elim (plus_comm y z).
-rewrite plus_assoc.
-rewrite H.
-rewrite plus_zero_left.
-reflexivity.
-Qed.
-
-Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y.
-intros.
-apply (aux2 (x:=(x * y)));
- [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ].
-Qed.
-Hint Resolve Th_opp_mult_left.
-
-Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y).
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_zero_right : forall n:A, n * 0 = 0.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_plus_zero_right : forall n:A, n + 0 = n.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma Th_plus_zero_right2 : forall n:A, n = n + 0.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma Th_mult_one_right : forall n:A, n * 1 = n.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_mult_one_right2 : forall n:A, n = n * 1.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y.
-intros; do 2 rewrite (mult_comm x); auto.
-Qed.
-
-Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y).
-intros; do 2 rewrite (mult_comm x); auto.
-Qed.
-
-Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y).
-intros.
-apply (aux2 (x:=(x + y)));
- [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc;
-    rewrite opp_def; rewrite plus_zero_left; auto
- | auto ].
-Qed.
-
-Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p).
-eauto. Qed.
-
-Lemma Th_opp_opp : forall n:A, - - n = n.
-intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ].
-Qed.
-Hint Resolve Th_opp_opp.
-
-Lemma Th_opp_opp2 : forall n:A, n = - - n.
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y.
-intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto.
-Qed.
-
-Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y.
-symmetry ; apply Th_mult_opp_opp. Qed.
-
-Lemma Th_opp_zero : - 0 = 0.
-rewrite <- (plus_zero_left (- 0)).
-auto. Qed.
-(*
-Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p.
-intros; generalize (f_equal (fun z => - n + z) H).
-repeat rewrite plus_assoc.
-rewrite (plus_comm (- n) n).
-rewrite opp_def.
-repeat rewrite Th_plus_zero_left; eauto.
-Qed.
-
-Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
-intros.
-eapply Th_plus_reg_left with n.
-rewrite (plus_comm n m).
-rewrite (plus_comm n p).
-auto.
-Qed.
-*)
-Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
-intros.
-repeat rewrite (mult_comm n).
-eauto.
-Qed.
-
-Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry ; apply Th_distr_right.
-Qed.
-
-End Theory_of_rings.
-
-Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core.
-
-Unset Implicit Arguments.
-
-Definition Semi_Ring_Theory_of :
-  forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A)
-    (Aopp:A -> A) (Aeq:A -> A -> bool),
-    Ring_Theory Aplus Amult Aone Azero Aopp Aeq ->
-    Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
-intros until 1; case H.
-split; intros; simpl; eauto.
-Defined.
-
-(* Every ring can be viewed as a semi-ring : this property will be used
-  in Abstract_polynom. *)
-Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory.
-
-
-Section product_ring.
-
-End product_ring.
-
-Section power_ring.
-
-End power_ring.
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
deleted file mode 100644
index 5c702c90e..000000000
--- a/plugins/ring/LegacyZArithRing.v
+++ /dev/null
@@ -1,35 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the binary integers of ZArith *)
-
-Require Export LegacyArithRing.
-Require Export ZArith_base.
-Require Import Eqdep_dec.
-Require Import LegacyRing.
-
-Definition Zeq (x y:Z) :=
-  match (x ?= y)%Z with
-  | Datatypes.Eq => true
-  | _ => false
-  end.
-
-Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
-  intros x y H; unfold Zeq in H.
-  apply Z.compare_eq.
-  destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ].
-Qed.
-
-Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq.
-  split; intros; eauto with zarith.
-  apply Zeq_prop; assumption.
-Qed.
-
-(* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory
- [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
deleted file mode 100644
index 7995696ff..000000000
--- a/plugins/ring/Ring_abstract.v
+++ /dev/null
@@ -1,700 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import LegacyRing_theory.
-Require Import Quote.
-Require Import Ring_normalize.
-
-Section abstract_semi_rings.
-
-Inductive aspolynomial : Type :=
-  | ASPvar : index -> aspolynomial
-  | ASP0 : aspolynomial
-  | ASP1 : aspolynomial
-  | ASPplus : aspolynomial -> aspolynomial -> aspolynomial
-  | ASPmult : aspolynomial -> aspolynomial -> aspolynomial.
-
-Inductive abstract_sum : Type :=
-  | Nil_acs : abstract_sum
-  | Cons_acs : varlist -> abstract_sum -> abstract_sum.
-
-Fixpoint abstract_sum_merge (s1:abstract_sum) :
- abstract_sum -> abstract_sum :=
-  match s1 with
-  | Cons_acs l1 t1 =>
-      (fix asm_aux (s2:abstract_sum) : abstract_sum :=
-         match s2 with
-         | Cons_acs l2 t2 =>
-             if varlist_lt l1 l2
-             then Cons_acs l1 (abstract_sum_merge t1 s2)
-             else Cons_acs l2 (asm_aux t2)
-         | Nil_acs => s1
-         end)
-  | Nil_acs => fun s2 => s2
-  end.
-
-Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} :
- abstract_sum :=
-  match s2 with
-  | Cons_acs l2 t2 =>
-      if varlist_lt l1 l2
-      then Cons_acs l1 s2
-      else Cons_acs l2 (abstract_varlist_insert l1 t2)
-  | Nil_acs => Cons_acs l1 Nil_acs
-  end.
-
-Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} :
- abstract_sum :=
-  match s2 with
-  | Cons_acs l2 t2 =>
-      abstract_varlist_insert (varlist_merge l1 l2)
-        (abstract_sum_scalar l1 t2)
-  | Nil_acs => Nil_acs
-  end.
-
-Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum :=
-  match s1 with
-  | Cons_acs l1 t1 =>
-      abstract_sum_merge (abstract_sum_scalar l1 s2)
-        (abstract_sum_prod t1 s2)
-  | Nil_acs => Nil_acs
-  end.
-
-Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum :=
-  match p with
-  | ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs
-  | ASP1 => Cons_acs Nil_var Nil_acs
-  | ASP0 => Nil_acs
-  | ASPplus l r =>
-      abstract_sum_merge (aspolynomial_normalize l)
-        (aspolynomial_normalize r)
-  | ASPmult l r =>
-      abstract_sum_prod (aspolynomial_normalize l) (aspolynomial_normalize r)
-  end.
-
-
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aeq : A -> A -> bool.
-Variable vm : varmap A.
-Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
-
-Fixpoint interp_asp (p:aspolynomial) : A :=
-  match p with
-  | ASPvar i => interp_var Azero vm i
-  | ASP0 => Azero
-  | ASP1 => Aone
-  | ASPplus l r => Aplus (interp_asp l) (interp_asp r)
-  | ASPmult l r => Amult (interp_asp l) (interp_asp r)
-  end.
-
-(* Local *) Definition iacs_aux :=
-              (fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A :=
-                 match s with
-                 | Nil_acs => a
-                 | Cons_acs l t =>
-                     Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t)
-                 end).
-
-Definition interp_acs (s:abstract_sum) : A :=
-  match s with
-  | Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t
-  | Nil_acs => Azero
-  end.
-
-Hint Resolve (SR_plus_comm T).
-Hint Resolve (SR_plus_assoc T).
-Hint Resolve (SR_plus_assoc2 T).
-Hint Resolve (SR_mult_comm T).
-Hint Resolve (SR_mult_assoc T).
-Hint Resolve (SR_mult_assoc2 T).
-Hint Resolve (SR_plus_zero_left T).
-Hint Resolve (SR_plus_zero_left2 T).
-Hint Resolve (SR_mult_one_left T).
-Hint Resolve (SR_mult_one_left2 T).
-Hint Resolve (SR_mult_zero_left T).
-Hint Resolve (SR_mult_zero_left2 T).
-Hint Resolve (SR_distr_left T).
-Hint Resolve (SR_distr_left2 T).
-(*Hint Resolve (SR_plus_reg_left T).*)
-Hint Resolve (SR_plus_permute T).
-Hint Resolve (SR_mult_permute T).
-Hint Resolve (SR_distr_right T).
-Hint Resolve (SR_distr_right2 T).
-Hint Resolve (SR_mult_zero_right T).
-Hint Resolve (SR_mult_zero_right2 T).
-Hint Resolve (SR_plus_zero_right T).
-Hint Resolve (SR_plus_zero_right2 T).
-Hint Resolve (SR_mult_one_right T).
-Hint Resolve (SR_mult_one_right2 T).
-(*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-Remark iacs_aux_ok :
- forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s).
-Proof.
-  simple induction s; simpl; intros.
-  trivial.
-  reflexivity.
-Qed.
-
-Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core.
-
-Lemma abstract_varlist_insert_ok :
- forall (l:varlist) (s:abstract_sum),
-   interp_acs (abstract_varlist_insert l s) =
-   Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s).
-
-  simple induction s.
-  trivial.
-
-  simpl; intros.
-  elim (varlist_lt l v); simpl.
-  eauto.
-  rewrite iacs_aux_ok.
-  rewrite H; auto.
-
-Qed.
-
-Lemma abstract_sum_merge_ok :
- forall x y:abstract_sum,
-   interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y).
-
-Proof.
-  simple induction x.
-  trivial.
-  simple induction y; intros.
-
-  auto.
-
-  simpl; elim (varlist_lt v v0); simpl.
-  repeat rewrite iacs_aux_ok.
-  rewrite H; simpl; auto.
-
-  simpl in H0.
-  repeat rewrite iacs_aux_ok.
-  rewrite H0. simpl; auto.
-Qed.
-
-Lemma abstract_sum_scalar_ok :
- forall (l:varlist) (s:abstract_sum),
-   interp_acs (abstract_sum_scalar l s) =
-   Amult (interp_vl Amult Aone Azero vm l) (interp_acs s).
-Proof.
-  simple induction s.
-  simpl; eauto.
-
-  simpl; intros.
-  rewrite iacs_aux_ok.
-  rewrite abstract_varlist_insert_ok.
-  rewrite H.
-  rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  auto.
-Qed.
-
-Lemma abstract_sum_prod_ok :
- forall x y:abstract_sum,
-   interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y).
-
-Proof.
-  simple induction x.
-  intros; simpl; eauto.
-
-  destruct y as [| v0 a0]; intros.
-
-  simpl; rewrite H; eauto.
-
-  unfold abstract_sum_prod; fold abstract_sum_prod.
-  rewrite abstract_sum_merge_ok.
-  rewrite abstract_sum_scalar_ok.
-  rewrite H; simpl; auto.
-Qed.
-
-Theorem aspolynomial_normalize_ok :
- forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x).
-Proof.
-  simple induction x; simpl; intros; trivial.
-  rewrite abstract_sum_merge_ok.
-  rewrite H; rewrite H0; eauto.
-  rewrite abstract_sum_prod_ok.
-  rewrite H; rewrite H0; eauto.
-Qed.
-
-End abstract_semi_rings.
-
-Section abstract_rings.
-
-(* In abstract polynomials there is no constants other
-   than 0 and 1. An abstract ring is a ring whose operations plus,
-   and mult are not functions but  constructors. In other words,
-   when c1 and c2 are closed,  (plus c1 c2) doesn't reduce to a closed
-   term. "closed" mean here "without plus and mult". *)
-
-(* this section is not parametrized by a (semi-)ring.
-   Nevertheless, they are two different types for semi-rings and rings
-   and there will be 2 correction theorems *)
-
-Inductive apolynomial : Type :=
-  | APvar : index -> apolynomial
-  | AP0 : apolynomial
-  | AP1 : apolynomial
-  | APplus : apolynomial -> apolynomial -> apolynomial
-  | APmult : apolynomial -> apolynomial -> apolynomial
-  | APopp : apolynomial -> apolynomial.
-
-(* A canonical "abstract" sum is a list of varlist with the sign "+" or "-".
-   Invariant : the list is sorted and there is no varlist is present
-   with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *)
-
-Inductive signed_sum : Type :=
-  | Nil_varlist : signed_sum
-  | Plus_varlist : varlist -> signed_sum -> signed_sum
-  | Minus_varlist : varlist -> signed_sum -> signed_sum.
-
-Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum :=
-  match s1 with
-  | Plus_varlist l1 t1 =>
-      (fix ssm_aux (s2:signed_sum) : signed_sum :=
-         match s2 with
-         | Plus_varlist l2 t2 =>
-             if varlist_lt l1 l2
-             then Plus_varlist l1 (signed_sum_merge t1 s2)
-             else Plus_varlist l2 (ssm_aux t2)
-         | Minus_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then signed_sum_merge t1 t2
-             else
-              if varlist_lt l1 l2
-              then Plus_varlist l1 (signed_sum_merge t1 s2)
-              else Minus_varlist l2 (ssm_aux t2)
-         | Nil_varlist => s1
-         end)
-  | Minus_varlist l1 t1 =>
-      (fix ssm_aux2 (s2:signed_sum) : signed_sum :=
-         match s2 with
-         | Plus_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then signed_sum_merge t1 t2
-             else
-              if varlist_lt l1 l2
-              then Minus_varlist l1 (signed_sum_merge t1 s2)
-              else Plus_varlist l2 (ssm_aux2 t2)
-         | Minus_varlist l2 t2 =>
-             if varlist_lt l1 l2
-             then Minus_varlist l1 (signed_sum_merge t1 s2)
-             else Minus_varlist l2 (ssm_aux2 t2)
-         | Nil_varlist => s1
-         end)
-  | Nil_varlist => fun s2 => s2
-  end.
-
-Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
-  match s2 with
-  | Plus_varlist l2 t2 =>
-      if varlist_lt l1 l2
-      then Plus_varlist l1 s2
-      else Plus_varlist l2 (plus_varlist_insert l1 t2)
-  | Minus_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then t2
-      else
-       if varlist_lt l1 l2
-       then Plus_varlist l1 s2
-       else Minus_varlist l2 (plus_varlist_insert l1 t2)
-  | Nil_varlist => Plus_varlist l1 Nil_varlist
-  end.
-
-Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
-  match s2 with
-  | Plus_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then t2
-      else
-       if varlist_lt l1 l2
-       then Minus_varlist l1 s2
-       else Plus_varlist l2 (minus_varlist_insert l1 t2)
-  | Minus_varlist l2 t2 =>
-      if varlist_lt l1 l2
-      then Minus_varlist l1 s2
-      else Minus_varlist l2 (minus_varlist_insert l1 t2)
-  | Nil_varlist => Minus_varlist l1 Nil_varlist
-  end.
-
-Fixpoint signed_sum_opp (s:signed_sum) : signed_sum :=
-  match s with
-  | Plus_varlist l2 t2 => Minus_varlist l2 (signed_sum_opp t2)
-  | Minus_varlist l2 t2 => Plus_varlist l2 (signed_sum_opp t2)
-  | Nil_varlist => Nil_varlist
-  end.
-
-
-Fixpoint plus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
-  match s2 with
-  | Plus_varlist l2 t2 =>
-      plus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2)
-  | Minus_varlist l2 t2 =>
-      minus_varlist_insert (varlist_merge l1 l2) (plus_sum_scalar l1 t2)
-  | Nil_varlist => Nil_varlist
-  end.
-
-Fixpoint minus_sum_scalar (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
-  match s2 with
-  | Plus_varlist l2 t2 =>
-      minus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2)
-  | Minus_varlist l2 t2 =>
-      plus_varlist_insert (varlist_merge l1 l2) (minus_sum_scalar l1 t2)
-  | Nil_varlist => Nil_varlist
-  end.
-
-Fixpoint signed_sum_prod (s1 s2:signed_sum) {struct s1} : signed_sum :=
-  match s1 with
-  | Plus_varlist l1 t1 =>
-      signed_sum_merge (plus_sum_scalar l1 s2) (signed_sum_prod t1 s2)
-  | Minus_varlist l1 t1 =>
-      signed_sum_merge (minus_sum_scalar l1 s2) (signed_sum_prod t1 s2)
-  | Nil_varlist => Nil_varlist
-  end.
-
-Fixpoint apolynomial_normalize (p:apolynomial) : signed_sum :=
-  match p with
-  | APvar i => Plus_varlist (Cons_var i Nil_var) Nil_varlist
-  | AP1 => Plus_varlist Nil_var Nil_varlist
-  | AP0 => Nil_varlist
-  | APplus l r =>
-      signed_sum_merge (apolynomial_normalize l) (apolynomial_normalize r)
-  | APmult l r =>
-      signed_sum_prod (apolynomial_normalize l) (apolynomial_normalize r)
-  | APopp q => signed_sum_opp (apolynomial_normalize q)
-  end.
-
-
-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.
-Variable vm : varmap A.
-Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
-
-(* Local *) Definition isacs_aux :=
-              (fix isacs_aux (a:A) (s:signed_sum) {struct s} : A :=
-                 match s with
-                 | Nil_varlist => a
-                 | Plus_varlist l t =>
-                     Aplus a (isacs_aux (interp_vl Amult Aone Azero vm l) t)
-                 | Minus_varlist l t =>
-                     Aplus a
-                       (isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t)
-                 end).
-
-Definition interp_sacs (s:signed_sum) : A :=
-  match s with
-  | Plus_varlist l t => isacs_aux (interp_vl Amult Aone Azero vm l) t
-  | Minus_varlist l t => isacs_aux (Aopp (interp_vl Amult Aone Azero vm l)) t
-  | Nil_varlist => Azero
-  end.
-
-Fixpoint interp_ap (p:apolynomial) : A :=
-  match p with
-  | APvar i => interp_var Azero vm i
-  | AP0 => Azero
-  | AP1 => Aone
-  | APplus l r => Aplus (interp_ap l) (interp_ap r)
-  | APmult l r => Amult (interp_ap l) (interp_ap r)
-  | APopp q => Aopp (interp_ap q)
-  end.
-
-Hint Resolve (Th_plus_comm T).
-Hint Resolve (Th_plus_assoc T).
-Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_comm T).
-Hint Resolve (Th_mult_assoc T).
-Hint Resolve (Th_mult_assoc2 T).
-Hint Resolve (Th_plus_zero_left T).
-Hint Resolve (Th_plus_zero_left2 T).
-Hint Resolve (Th_mult_one_left T).
-Hint Resolve (Th_mult_one_left2 T).
-Hint Resolve (Th_mult_zero_left T).
-Hint Resolve (Th_mult_zero_left2 T).
-Hint Resolve (Th_distr_left T).
-Hint Resolve (Th_distr_left2 T).
-(*Hint Resolve (Th_plus_reg_left T).*)
-Hint Resolve (Th_plus_permute T).
-Hint Resolve (Th_mult_permute T).
-Hint Resolve (Th_distr_right T).
-Hint Resolve (Th_distr_right2 T).
-Hint Resolve (Th_mult_zero_right2 T).
-Hint Resolve (Th_plus_zero_right T).
-Hint Resolve (Th_plus_zero_right2 T).
-Hint Resolve (Th_mult_one_right T).
-Hint Resolve (Th_mult_one_right2 T).
-(*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-Lemma isacs_aux_ok :
- forall (x:A) (s:signed_sum), isacs_aux x s = Aplus x (interp_sacs s).
-Proof.
-  simple induction s; simpl; intros.
-  trivial.
-  reflexivity.
-  reflexivity.
-Qed.
-
-Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core.
-
-Ltac solve1 v v0 H H0 :=
-  simpl; elim (varlist_lt v v0); simpl; rewrite isacs_aux_ok;
-   [ rewrite H; simpl; auto | simpl in H0; rewrite H0; auto ].
-
-Lemma signed_sum_merge_ok :
- forall x y:signed_sum,
-   interp_sacs (signed_sum_merge x y) = Aplus (interp_sacs x) (interp_sacs y).
-
-  simple induction x.
-  intro; simpl; auto.
-
-  simple induction y; intros.
-
-  auto.
-
-  solve1 v v0 H H0.
-
-  simpl; generalize (varlist_eq_prop v v0).
-  elim (varlist_eq v v0); simpl.
-
-  intro Heq; rewrite (Heq I).
-  rewrite H.
-  repeat rewrite isacs_aux_ok.
-  rewrite (Th_plus_permute T).
-  repeat rewrite (Th_plus_assoc T).
-  rewrite
-   (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v0))
-      (interp_vl Amult Aone Azero vm v0)).
-  rewrite (Th_opp_def T).
-  rewrite (Th_plus_zero_left T).
-  reflexivity.
-
-  solve1 v v0 H H0.
-
-  simple induction y; intros.
-
-  auto.
-
-  simpl; generalize (varlist_eq_prop v v0).
-  elim (varlist_eq v v0); simpl.
-
-  intro Heq; rewrite (Heq I).
-  rewrite H.
-  repeat rewrite isacs_aux_ok.
-  rewrite (Th_plus_permute T).
-  repeat rewrite (Th_plus_assoc T).
-  rewrite (Th_opp_def T).
-  rewrite (Th_plus_zero_left T).
-  reflexivity.
-
-  solve1 v v0 H H0.
-
-  solve1 v v0 H H0.
-
-Qed.
-
-Ltac solve2 l v H :=
-  elim (varlist_lt l v); simpl; rewrite isacs_aux_ok;
-   [ auto | rewrite H; auto ].
-
-Lemma plus_varlist_insert_ok :
- forall (l:varlist) (s:signed_sum),
-   interp_sacs (plus_varlist_insert l s) =
-   Aplus (interp_vl Amult Aone Azero vm l) (interp_sacs s).
-Proof.
-
-  simple induction s.
-  trivial.
-
-  simpl; intros.
-  solve2 l v H.
-
-  simpl; intros.
-  generalize (varlist_eq_prop l v).
-  elim (varlist_eq l v); simpl.
-
-  intro Heq; rewrite (Heq I).
-  repeat rewrite isacs_aux_ok.
-  repeat rewrite (Th_plus_assoc T).
-  rewrite (Th_opp_def T).
-  rewrite (Th_plus_zero_left T).
-  reflexivity.
-
-  solve2 l v H.
-
-Qed.
-
-Lemma minus_varlist_insert_ok :
- forall (l:varlist) (s:signed_sum),
-   interp_sacs (minus_varlist_insert l s) =
-   Aplus (Aopp (interp_vl Amult Aone Azero vm l)) (interp_sacs s).
-Proof.
-
-  simple induction s.
-  trivial.
-
-  simpl; intros.
-  generalize (varlist_eq_prop l v).
-  elim (varlist_eq l v); simpl.
-
-  intro Heq; rewrite (Heq I).
-  repeat rewrite isacs_aux_ok.
-  repeat rewrite (Th_plus_assoc T).
-  rewrite
-   (Th_plus_comm T (Aopp (interp_vl Amult Aone Azero vm v))
-      (interp_vl Amult Aone Azero vm v)).
-  rewrite (Th_opp_def T).
-  auto.
-
-  simpl; intros.
-  solve2 l v H.
-
-  simpl; intros; solve2 l v H.
-
-Qed.
-
-Lemma signed_sum_opp_ok :
- forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s).
-Proof.
-
-  simple induction s; simpl; intros.
-
-  symmetry ; apply (Th_opp_zero T).
-
-  repeat rewrite isacs_aux_ok.
-  rewrite H.
-  rewrite (Th_plus_opp_opp T).
-  reflexivity.
-
-  repeat rewrite isacs_aux_ok.
-  rewrite H.
-  rewrite <- (Th_plus_opp_opp T).
-  rewrite (Th_opp_opp T).
-  reflexivity.
-
-Qed.
-
-Lemma plus_sum_scalar_ok :
- forall (l:varlist) (s:signed_sum),
-   interp_sacs (plus_sum_scalar l s) =
-   Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s).
-Proof.
-
-  simple induction s.
-  trivial.
-
-  simpl; intros.
-  rewrite plus_varlist_insert_ok.
-  rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  repeat rewrite isacs_aux_ok.
-  rewrite H.
-  auto.
-
-  simpl; intros.
-  rewrite minus_varlist_insert_ok.
-  repeat rewrite isacs_aux_ok.
-  rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  rewrite H.
-  rewrite (Th_distr_right T).
-  rewrite <- (Th_opp_mult_right T).
-  reflexivity.
-
-Qed.
-
-Lemma minus_sum_scalar_ok :
- forall (l:varlist) (s:signed_sum),
-   interp_sacs (minus_sum_scalar l s) =
-   Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)).
-Proof.
-
-  simple induction s; simpl; intros.
-
-  rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T).
-
-  simpl; intros.
-  rewrite minus_varlist_insert_ok.
-  rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  repeat rewrite isacs_aux_ok.
-  rewrite H.
-  rewrite (Th_distr_right T).
-  rewrite (Th_plus_opp_opp T).
-  reflexivity.
-
-  simpl; intros.
-  rewrite plus_varlist_insert_ok.
-  repeat rewrite isacs_aux_ok.
-  rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
-  rewrite H.
-  rewrite (Th_distr_right T).
-  rewrite <- (Th_opp_mult_right T).
-  rewrite <- (Th_plus_opp_opp T).
-  rewrite (Th_opp_opp T).
-  reflexivity.
-
-Qed.
-
-Lemma signed_sum_prod_ok :
- forall x y:signed_sum,
-   interp_sacs (signed_sum_prod x y) = Amult (interp_sacs x) (interp_sacs y).
-Proof.
-
-  simple induction x.
-
-  simpl; eauto 1.
-
-  intros; simpl.
-  rewrite signed_sum_merge_ok.
-  rewrite plus_sum_scalar_ok.
-  repeat rewrite isacs_aux_ok.
-  rewrite H.
-  auto.
-
-  intros; simpl.
-  repeat rewrite isacs_aux_ok.
-  rewrite signed_sum_merge_ok.
-  rewrite minus_sum_scalar_ok.
-  rewrite H.
-  rewrite (Th_distr_left T).
-  rewrite (Th_opp_mult_left T).
-  reflexivity.
-
-Qed.
-
-Theorem apolynomial_normalize_ok :
- forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p.
-Proof.
-  simple induction p; simpl; auto 1.
-  intros.
-    rewrite signed_sum_merge_ok.
-    rewrite H; rewrite H0; reflexivity.
-  intros.
-    rewrite signed_sum_prod_ok.
-    rewrite H; rewrite H0; reflexivity.
-  intros.
-    rewrite signed_sum_opp_ok.
-    rewrite H; reflexivity.
-Qed.
-
-End abstract_rings.
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
deleted file mode 100644
index 0d8393f76..000000000
--- a/plugins/ring/Ring_normalize.v
+++ /dev/null
@@ -1,897 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import LegacyRing_theory.
-Require Import Quote.
-
-Set Implicit Arguments.
-
-Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
-Proof.
-  intros.
-  apply index_eq_prop.
-  generalize H.
-  case (index_eq n m); simpl; trivial; intros.
-  contradiction.
-Qed.
-
-Section semi_rings.
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aeq : A -> A -> bool.
-
-(* Section definitions. *)
-
-
-(******************************************)
-(* Normal abtract Polynomials             *)
-(******************************************)
-(* DEFINITIONS :
-- A varlist is a sorted product of one or more variables : x, x*y*z
-- A monom is a constant, a varlist or the product of a constant by a varlist
-  variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
-- A canonical sum is either a monom or an ordered sum of monoms
-  (the order on monoms is defined later)
-- A normal polynomial it either a constant or a canonical sum or a constant
-  plus a canonical sum
-*)
-
-(* varlist is isomorphic to (list var), but we built a special inductive
-   for efficiency *)
-Inductive varlist : Type :=
-  | Nil_var : varlist
-  | Cons_var : index -> varlist -> varlist.
-
-Inductive canonical_sum : Type :=
-  | Nil_monom : canonical_sum
-  | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
-  | Cons_varlist : varlist -> canonical_sum -> canonical_sum.
-
-(* Order on monoms *)
-
-(* That's the lexicographic order on varlist, extended by :
-  - A constant is less than every monom
-  - The relation between two varlist is preserved by multiplication by a
-  constant.
-
-  Examples :
-  3 < x < y
-  x*y < x*y*y*z
-  2*x*y < x*y*y*z
-  x*y < 54*x*y*y*z
-  4*x*y < 59*x*y*y*z
-*)
-
-Fixpoint varlist_eq (x y:varlist) {struct y} : bool :=
-  match x, y with
-  | Nil_var, Nil_var => true
-  | Cons_var i xrest, Cons_var j yrest =>
-      andb (index_eq i j) (varlist_eq xrest yrest)
-  | _, _ => false
-  end.
-
-Fixpoint varlist_lt (x y:varlist) {struct y} : bool :=
-  match x, y with
-  | Nil_var, Cons_var _ _ => true
-  | Cons_var i xrest, Cons_var j yrest =>
-      if index_lt i j
-      then true
-      else andb (index_eq i j) (varlist_lt xrest yrest)
-  | _, _ => false
-  end.
-
-(* merges two variables lists *)
-Fixpoint varlist_merge (l1:varlist) : varlist -> varlist :=
-  match l1 with
-  | Cons_var v1 t1 =>
-      (fix vm_aux (l2:varlist) : varlist :=
-         match l2 with
-         | Cons_var v2 t2 =>
-             if index_lt v1 v2
-             then Cons_var v1 (varlist_merge t1 l2)
-             else Cons_var v2 (vm_aux t2)
-         | Nil_var => l1
-         end)
-  | Nil_var => fun l2 => l2
-  end.
-
-(* returns the sum of two canonical sums  *)
-Fixpoint canonical_sum_merge (s1:canonical_sum) :
- canonical_sum -> canonical_sum :=
-  match s1 with
-  | Cons_monom c1 l1 t1 =>
-      (fix csm_aux (s2:canonical_sum) : canonical_sum :=
-         match s2 with
-         | Cons_monom c2 l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
-              else Cons_monom c2 l2 (csm_aux t2)
-         | Cons_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
-              else Cons_varlist l2 (csm_aux t2)
-         | Nil_monom => s1
-         end)
-  | Cons_varlist l1 t1 =>
-      (fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
-         match s2 with
-         | Cons_monom c2 l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_varlist l1 (canonical_sum_merge t1 s2)
-              else Cons_monom c2 l2 (csm_aux2 t2)
-         | Cons_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_varlist l1 (canonical_sum_merge t1 s2)
-              else Cons_varlist l2 (csm_aux2 t2)
-         | Nil_monom => s1
-         end)
-  | Nil_monom => fun s2 => s2
-  end.
-
-(* Insertion of a monom in a canonical sum *)
-Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} :
- canonical_sum :=
-  match s2 with
-  | Cons_monom c2 l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus c1 c2) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_monom c1 l1 s2
-       else Cons_monom c2 l2 (monom_insert c1 l1 t2)
-  | Cons_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus c1 Aone) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_monom c1 l1 s2
-       else Cons_varlist l2 (monom_insert c1 l1 t2)
-  | Nil_monom => Cons_monom c1 l1 Nil_monom
-  end.
-
-Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} :
- canonical_sum :=
-  match s2 with
-  | Cons_monom c2 l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus Aone c2) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_varlist l1 s2
-       else Cons_monom c2 l2 (varlist_insert l1 t2)
-  | Cons_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus Aone Aone) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_varlist l1 s2
-       else Cons_varlist l2 (varlist_insert l1 t2)
-  | Nil_monom => Cons_varlist l1 Nil_monom
-  end.
-
-(* Computes c0*s *)
-Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} :
- canonical_sum :=
-  match s with
-  | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t)
-  | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* Computes l0*s  *)
-Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} :
- canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
-  | Cons_varlist l t =>
-      varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* Computes c0*l0*s  *)
-Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist)
- (s:canonical_sum) {struct s} : canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      monom_insert (Amult c0 c) (varlist_merge l0 l)
-        (canonical_sum_scalar3 c0 l0 t)
-  | Cons_varlist l t =>
-      monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* returns the product of two canonical sums *)
-Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} :
- canonical_sum :=
-  match s1 with
-  | Cons_monom c1 l1 t1 =>
-      canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2)
-        (canonical_sum_prod t1 s2)
-  | Cons_varlist l1 t1 =>
-      canonical_sum_merge (canonical_sum_scalar2 l1 s2)
-        (canonical_sum_prod t1 s2)
-  | Nil_monom => Nil_monom
-  end.
-
-(* The type to represent concrete semi-ring polynomials *)
-Inductive spolynomial : Type :=
-  | SPvar : index -> spolynomial
-  | SPconst : A -> spolynomial
-  | SPplus : spolynomial -> spolynomial -> spolynomial
-  | SPmult : spolynomial -> spolynomial -> spolynomial.
-
-Fixpoint spolynomial_normalize (p:spolynomial) : canonical_sum :=
-  match p with
-  | SPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
-  | SPconst c => Cons_monom c Nil_var Nil_monom
-  | SPplus l r =>
-      canonical_sum_merge (spolynomial_normalize l) (spolynomial_normalize r)
-  | SPmult l r =>
-      canonical_sum_prod (spolynomial_normalize l) (spolynomial_normalize r)
-  end.
-
-(* Deletion of useless 0 and 1 in canonical sums *)
-Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      if Aeq c Azero
-      then canonical_sum_simplify t
-      else
-       if Aeq c Aone
-       then Cons_varlist l (canonical_sum_simplify t)
-       else Cons_monom c l (canonical_sum_simplify t)
-  | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t)
-  | Nil_monom => Nil_monom
-  end.
-
-Definition spolynomial_simplify (x:spolynomial) :=
-  canonical_sum_simplify (spolynomial_normalize x).
-
-(* End definitions. *)
-
-(* Section interpretation. *)
-
-(*** Here a variable map is defined and the interpetation of a spolynom
-  acording to a certain variables map. Once again the choosen definition
-  is generic and could be changed ****)
-
-Variable vm : varmap A.
-
-(* Interpretation of list of variables
- * [x1; ... ; xn ] is interpreted as (find v x1)* ... *(find v xn)
- * The unbound variables are mapped to 0. Normally this case sould
- * never occur. Since we want only to prove correctness theorems, which form
- * is : for any varmap and any spolynom ... this is a safe and pain-saving
- * choice *)
-Definition interp_var (i:index) := varmap_find Azero i vm.
-
-(* Local *) Definition ivl_aux :=
-              (fix ivl_aux (x:index) (t:varlist) {struct t} : A :=
-                 match t with
-                 | Nil_var => interp_var x
-                 | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t')
-                 end).
-
-Definition interp_vl (l:varlist) :=
-  match l with
-  | Nil_var => Aone
-  | Cons_var x t => ivl_aux x t
-  end.
-
-(* Local *) Definition interp_m (c:A) (l:varlist) :=
-              match l with
-              | Nil_var => c
-              | Cons_var x t => Amult c (ivl_aux x t)
-              end.
-
-(* Local *) Definition ics_aux :=
-              (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A :=
-                 match s with
-                 | Nil_monom => a
-                 | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t)
-                 | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t)
-                 end).
-
-(* Interpretation of a canonical sum *)
-Definition interp_cs (s:canonical_sum) : A :=
-  match s with
-  | Nil_monom => Azero
-  | Cons_varlist l t => ics_aux (interp_vl l) t
-  | Cons_monom c l t => ics_aux (interp_m c l) t
-  end.
-
-Fixpoint interp_sp (p:spolynomial) : A :=
-  match p with
-  | SPconst c => c
-  | SPvar i => interp_var i
-  | SPplus p1 p2 => Aplus (interp_sp p1) (interp_sp p2)
-  | SPmult p1 p2 => Amult (interp_sp p1) (interp_sp p2)
-  end.
-
-
-(* End interpretation. *)
-
-Unset Implicit Arguments.
-
-(* Section properties. *)
-
-Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
-
-Hint Resolve (SR_plus_comm T).
-Hint Resolve (SR_plus_assoc T).
-Hint Resolve (SR_plus_assoc2 T).
-Hint Resolve (SR_mult_comm T).
-Hint Resolve (SR_mult_assoc T).
-Hint Resolve (SR_mult_assoc2 T).
-Hint Resolve (SR_plus_zero_left T).
-Hint Resolve (SR_plus_zero_left2 T).
-Hint Resolve (SR_mult_one_left T).
-Hint Resolve (SR_mult_one_left2 T).
-Hint Resolve (SR_mult_zero_left T).
-Hint Resolve (SR_mult_zero_left2 T).
-Hint Resolve (SR_distr_left T).
-Hint Resolve (SR_distr_left2 T).
-(*Hint Resolve (SR_plus_reg_left T).*)
-Hint Resolve (SR_plus_permute T).
-Hint Resolve (SR_mult_permute T).
-Hint Resolve (SR_distr_right T).
-Hint Resolve (SR_distr_right2 T).
-Hint Resolve (SR_mult_zero_right T).
-Hint Resolve (SR_mult_zero_right2 T).
-Hint Resolve (SR_plus_zero_right T).
-Hint Resolve (SR_plus_zero_right2 T).
-Hint Resolve (SR_mult_one_right T).
-Hint Resolve (SR_mult_one_right2 T).
-(*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
-Proof.
-  simple induction x; simple induction y; contradiction || (try reflexivity).
-  simpl; intros.
-  generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
-  rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
-Qed.
-
-Remark ivl_aux_ok :
- forall (v:varlist) (i:index),
-   ivl_aux i v = Amult (interp_var i) (interp_vl v).
-Proof.
-  simple induction v; simpl; intros.
-  trivial.
-  rewrite H; trivial.
-Qed.
-
-Lemma varlist_merge_ok :
- forall x y:varlist,
-   interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y).
-Proof.
-  simple induction x.
-  simpl; trivial.
-  simple induction y.
-  simpl; trivial.
-  simpl; intros.
-  elim (index_lt i i0); simpl; intros.
-
-  repeat rewrite ivl_aux_ok.
-  rewrite H. simpl.
-  rewrite ivl_aux_ok.
-  eauto.
-
-  repeat rewrite ivl_aux_ok.
-  rewrite H0.
-  rewrite ivl_aux_ok.
-  eauto.
-Qed.
-
-Remark ics_aux_ok :
- forall (x:A) (s:canonical_sum), ics_aux x s = Aplus x (interp_cs s).
-Proof.
-  simple induction s; simpl; intros.
-  trivial.
-  reflexivity.
-  reflexivity.
-Qed.
-
-Remark interp_m_ok :
- forall (x:A) (l:varlist), interp_m x l = Amult x (interp_vl l).
-Proof.
-  destruct l as [| i v].
-  simpl; trivial.
-  reflexivity.
-Qed.
-
-Lemma canonical_sum_merge_ok :
- forall x y:canonical_sum,
-   interp_cs (canonical_sum_merge x y) = Aplus (interp_cs x) (interp_cs y).
-
-simple induction x; simpl.
-trivial.
-
-simple induction y; simpl; intros.
-(* monom and nil *)
-eauto.
-
-(* monom and monom *)
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl; repeat rewrite ics_aux_ok; rewrite H.
-repeat rewrite interp_m_ok.
-rewrite (SR_distr_left T).
-repeat rewrite <- (SR_plus_assoc T).
-apply f_equal with (f := Aplus (Amult a (interp_vl v0))).
-trivial.
-
-elim (varlist_lt v v0); simpl.
-repeat rewrite ics_aux_ok.
-rewrite H; simpl; rewrite ics_aux_ok; eauto.
-
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl;
- eauto.
-
-(* monom and varlist *)
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl; repeat rewrite ics_aux_ok; rewrite H.
-repeat rewrite interp_m_ok.
-rewrite (SR_distr_left T).
-repeat rewrite <- (SR_plus_assoc T).
-apply f_equal with (f := Aplus (Amult a (interp_vl v0))).
-rewrite (SR_mult_one_left T).
-trivial.
-
-elim (varlist_lt v v0); simpl.
-repeat rewrite ics_aux_ok.
-rewrite H; simpl; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl;
- eauto.
-
-simple induction y; simpl; intros.
-(* varlist and nil *)
-trivial.
-
-(* varlist and monom *)
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl; repeat rewrite ics_aux_ok; rewrite H.
-repeat rewrite interp_m_ok.
-rewrite (SR_distr_left T).
-repeat rewrite <- (SR_plus_assoc T).
-rewrite (SR_mult_one_left T).
-apply f_equal with (f := Aplus (interp_vl v0)).
-trivial.
-
-elim (varlist_lt v v0); simpl.
-repeat rewrite ics_aux_ok.
-rewrite H; simpl; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl;
- eauto.
-
-(* varlist and varlist *)
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl; repeat rewrite ics_aux_ok; rewrite H.
-repeat rewrite interp_m_ok.
-rewrite (SR_distr_left T).
-repeat rewrite <- (SR_plus_assoc T).
-rewrite (SR_mult_one_left T).
-apply f_equal with (f := Aplus (interp_vl v0)).
-trivial.
-
-elim (varlist_lt v v0); simpl.
-repeat rewrite ics_aux_ok.
-rewrite H; simpl; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl;
- eauto.
-Qed.
-
-Lemma monom_insert_ok :
- forall (a:A) (l:varlist) (s:canonical_sum),
-   interp_cs (monom_insert a l s) =
-   Aplus (Amult a (interp_vl l)) (interp_cs s).
-intros; generalize s; simple induction s0.
-
-simpl; rewrite interp_m_ok; trivial.
-
-simpl; intros.
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok;
- repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T);
- eauto.
-elim (varlist_lt l v); simpl;
- [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
- | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
-    rewrite ics_aux_ok; eauto ].
-
-simpl; intros.
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok;
- repeat rewrite ics_aux_ok; rewrite (SR_distr_left T);
- rewrite (SR_mult_one_left T); eauto.
-elim (varlist_lt l v); simpl;
- [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
- | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
-    rewrite ics_aux_ok; eauto ].
-Qed.
-
-Lemma varlist_insert_ok :
- forall (l:varlist) (s:canonical_sum),
-   interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s).
-intros; generalize s; simple induction s0.
-
-simpl; trivial.
-
-simpl; intros.
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok;
- repeat rewrite ics_aux_ok; rewrite interp_m_ok; rewrite (SR_distr_left T);
- rewrite (SR_mult_one_left T); eauto.
-elim (varlist_lt l v); simpl;
- [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
- | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
-    rewrite ics_aux_ok; eauto ].
-
-simpl; intros.
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl; rewrite interp_m_ok;
- repeat rewrite ics_aux_ok; rewrite (SR_distr_left T);
- rewrite (SR_mult_one_left T); eauto.
-elim (varlist_lt l v); simpl;
- [ repeat rewrite interp_m_ok; rewrite ics_aux_ok; eauto
- | repeat rewrite interp_m_ok; rewrite ics_aux_ok; rewrite H;
-    rewrite ics_aux_ok; eauto ].
-Qed.
-
-Lemma canonical_sum_scalar_ok :
- forall (a:A) (s:canonical_sum),
-   interp_cs (canonical_sum_scalar a s) = Amult a (interp_cs s).
-simple induction s.
-simpl; eauto.
-
-simpl; intros.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-reflexivity.
-
-simpl; intros.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-reflexivity.
-Qed.
-
-Lemma canonical_sum_scalar2_ok :
- forall (l:varlist) (s:canonical_sum),
-   interp_cs (canonical_sum_scalar2 l s) = Amult (interp_vl l) (interp_cs s).
-simple induction s.
-simpl; trivial.
-
-simpl; intros.
-rewrite monom_insert_ok.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite varlist_merge_ok.
-repeat rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-repeat rewrite <- (SR_plus_assoc T).
-rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
-reflexivity.
-
-simpl; intros.
-rewrite varlist_insert_ok.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite varlist_merge_ok.
-repeat rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-repeat rewrite <- (SR_plus_assoc T).
-reflexivity.
-Qed.
-
-Lemma canonical_sum_scalar3_ok :
- forall (c:A) (l:varlist) (s:canonical_sum),
-   interp_cs (canonical_sum_scalar3 c l s) =
-   Amult c (Amult (interp_vl l) (interp_cs s)).
-simple induction s.
-simpl; repeat rewrite (SR_mult_zero_right T); reflexivity.
-
-simpl; intros.
-rewrite monom_insert_ok.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite varlist_merge_ok.
-repeat rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-repeat rewrite <- (SR_plus_assoc T).
-rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
-reflexivity.
-
-simpl; intros.
-rewrite monom_insert_ok.
-repeat rewrite ics_aux_ok.
-repeat rewrite interp_m_ok.
-rewrite H.
-rewrite varlist_merge_ok.
-repeat rewrite (SR_distr_right T).
-repeat rewrite <- (SR_mult_assoc T).
-repeat rewrite <- (SR_plus_assoc T).
-rewrite (SR_mult_permute T c (interp_vl l) (interp_vl v)).
-reflexivity.
-Qed.
-
-Lemma canonical_sum_prod_ok :
- forall x y:canonical_sum,
-   interp_cs (canonical_sum_prod x y) = Amult (interp_cs x) (interp_cs y).
-simple induction x; simpl; intros.
-trivial.
-
-rewrite canonical_sum_merge_ok.
-rewrite canonical_sum_scalar3_ok.
-rewrite ics_aux_ok.
-rewrite interp_m_ok.
-rewrite H.
-rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)).
-symmetry .
-eauto.
-
-rewrite canonical_sum_merge_ok.
-rewrite canonical_sum_scalar2_ok.
-rewrite ics_aux_ok.
-rewrite H.
-trivial.
-Qed.
-
-Theorem spolynomial_normalize_ok :
- forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p.
-simple induction p; simpl; intros.
-
-reflexivity.
-reflexivity.
-
-rewrite canonical_sum_merge_ok.
-rewrite H; rewrite H0.
-reflexivity.
-
-rewrite canonical_sum_prod_ok.
-rewrite H; rewrite H0.
-reflexivity.
-Qed.
-
-Lemma canonical_sum_simplify_ok :
- forall s:canonical_sum, interp_cs (canonical_sum_simplify s) = interp_cs s.
-simple induction s.
-
-reflexivity.
-
-(* cons_monom *)
-simpl; intros.
-generalize (SR_eq_prop T a Azero).
-elim (Aeq a Azero).
-intro Heq; rewrite (Heq I).
-rewrite H.
-rewrite ics_aux_ok.
-rewrite interp_m_ok.
-rewrite (SR_mult_zero_left T).
-trivial.
-
-intros; simpl.
-generalize (SR_eq_prop T a Aone).
-elim (Aeq a Aone).
-intro Heq; rewrite (Heq I).
-simpl.
-repeat rewrite ics_aux_ok.
-rewrite interp_m_ok.
-rewrite H.
-rewrite (SR_mult_one_left T).
-reflexivity.
-
-simpl.
-repeat rewrite ics_aux_ok.
-rewrite interp_m_ok.
-rewrite H.
-reflexivity.
-
-(* cons_varlist *)
-simpl; intros.
-repeat rewrite ics_aux_ok.
-rewrite H.
-reflexivity.
-
-Qed.
-
-Theorem spolynomial_simplify_ok :
- forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p.
-intro.
-unfold spolynomial_simplify.
-rewrite canonical_sum_simplify_ok.
-apply spolynomial_normalize_ok.
-Qed.
-
-(* End properties. *)
-End semi_rings.
-
-Arguments Cons_varlist : default implicits.
-Arguments Cons_monom : default implicits.
-Arguments SPconst : default implicits.
-Arguments SPplus : default implicits.
-Arguments SPmult : default implicits.
-
-Section rings.
-
-(* Here the coercion between Ring and Semi-Ring will be useful *)
-
-Set Implicit Arguments.
-
-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.
-Variable vm : varmap A.
-Variable T : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
-
-Hint Resolve (Th_plus_comm T).
-Hint Resolve (Th_plus_assoc T).
-Hint Resolve (Th_plus_assoc2 T).
-Hint Resolve (Th_mult_comm T).
-Hint Resolve (Th_mult_assoc T).
-Hint Resolve (Th_mult_assoc2 T).
-Hint Resolve (Th_plus_zero_left T).
-Hint Resolve (Th_plus_zero_left2 T).
-Hint Resolve (Th_mult_one_left T).
-Hint Resolve (Th_mult_one_left2 T).
-Hint Resolve (Th_mult_zero_left T).
-Hint Resolve (Th_mult_zero_left2 T).
-Hint Resolve (Th_distr_left T).
-Hint Resolve (Th_distr_left2 T).
-(*Hint Resolve (Th_plus_reg_left T).*)
-Hint Resolve (Th_plus_permute T).
-Hint Resolve (Th_mult_permute T).
-Hint Resolve (Th_distr_right T).
-Hint Resolve (Th_distr_right2 T).
-Hint Resolve (Th_mult_zero_right T).
-Hint Resolve (Th_mult_zero_right2 T).
-Hint Resolve (Th_plus_zero_right T).
-Hint Resolve (Th_plus_zero_right2 T).
-Hint Resolve (Th_mult_one_right T).
-Hint Resolve (Th_mult_one_right2 T).
-(*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-(*** Definitions *)
-
-Inductive polynomial : Type :=
-  | Pvar : index -> polynomial
-  | Pconst : A -> polynomial
-  | Pplus : polynomial -> polynomial -> polynomial
-  | Pmult : polynomial -> polynomial -> polynomial
-  | Popp : polynomial -> polynomial.
-
-Fixpoint polynomial_normalize (x:polynomial) : canonical_sum A :=
-  match x with
-  | Pplus l r =>
-      canonical_sum_merge Aplus Aone (polynomial_normalize l)
-        (polynomial_normalize r)
-  | Pmult l r =>
-      canonical_sum_prod Aplus Amult Aone (polynomial_normalize l)
-        (polynomial_normalize r)
-  | Pconst c => Cons_monom c Nil_var (Nil_monom A)
-  | Pvar i => Cons_varlist (Cons_var i Nil_var) (Nil_monom A)
-  | Popp p =>
-      canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
-        (polynomial_normalize p)
-  end.
-
-Definition polynomial_simplify (x:polynomial) :=
-  canonical_sum_simplify Aone Azero Aeq (polynomial_normalize x).
-
-Fixpoint spolynomial_of (x:polynomial) : spolynomial A :=
-  match x with
-  | Pplus l r => SPplus (spolynomial_of l) (spolynomial_of r)
-  | Pmult l r => SPmult (spolynomial_of l) (spolynomial_of r)
-  | Pconst c => SPconst c
-  | Pvar i => SPvar A i
-  | Popp p => SPmult (SPconst (Aopp Aone)) (spolynomial_of p)
-  end.
-
-(*** Interpretation *)
-
-Fixpoint interp_p (p:polynomial) : A :=
-  match p with
-  | Pconst c => c
-  | Pvar i => varmap_find Azero i vm
-  | Pplus p1 p2 => Aplus (interp_p p1) (interp_p p2)
-  | Pmult p1 p2 => Amult (interp_p p1) (interp_p p2)
-  | Popp p1 => Aopp (interp_p p1)
-  end.
-
-(*** Properties *)
-
-Unset Implicit Arguments.
-
-Lemma spolynomial_of_ok :
- forall p:polynomial,
-   interp_p p = interp_sp Aplus Amult Azero vm (spolynomial_of p).
-simple induction p; reflexivity || (simpl; intros).
-rewrite H; rewrite H0; reflexivity.
-rewrite H; rewrite H0; reflexivity.
-rewrite H.
-rewrite (Th_opp_mult_left2 T).
-rewrite (Th_mult_one_left T).
-reflexivity.
-Qed.
-
-Theorem polynomial_normalize_ok :
- forall p:polynomial,
-   polynomial_normalize p =
-   spolynomial_normalize Aplus Amult Aone (spolynomial_of p).
-simple induction p; reflexivity || (simpl; intros).
-rewrite H; rewrite H0; reflexivity.
-rewrite H; rewrite H0; reflexivity.
-rewrite H; simpl.
-elim
- (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
-    (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0)));
- [ reflexivity
- | simpl; intros; rewrite H0; reflexivity
- | simpl; intros; rewrite H0; reflexivity ].
-Qed.
-
-Theorem polynomial_simplify_ok :
- forall p:polynomial,
-   interp_cs Aplus Amult Aone Azero vm (polynomial_simplify p) = interp_p p.
-intro.
-unfold polynomial_simplify.
-rewrite spolynomial_of_ok.
-rewrite polynomial_normalize_ok.
-rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T).
-rewrite (spolynomial_normalize_ok A Aplus Amult Aone Azero Aeq vm T).
-reflexivity.
-Qed.
-
-End rings.
-
-Infix "+" := Pplus : ring_scope.
-Infix "*" := Pmult : ring_scope.
-Notation "- x" := (Popp x) : ring_scope.
-Notation "[ x ]" := (Pvar x) (at level 0) : ring_scope.
-
-Delimit Scope ring_scope with ring.
diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v
deleted file mode 100644
index 106a946d3..000000000
--- a/plugins/ring/Setoid_ring.v
+++ /dev/null
@@ -1,12 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Setoid_ring_theory.
-Require Export Quote.
-Require Export Setoid_ring_normalize.
-Declare ML Module "ring_plugin".
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
deleted file mode 100644
index 59d86cede..000000000
--- a/plugins/ring/Setoid_ring_normalize.v
+++ /dev/null
@@ -1,1160 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import Setoid_ring_theory.
-Require Import Quote.
-
-Set Implicit Arguments.
-
-Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
-Proof.
-  simple induction n; simple induction m; simpl;
-   try reflexivity || contradiction.
-  intros; rewrite (H i0); trivial.
-  intros; rewrite (H i0); trivial.
-Qed.
-
-Section setoid.
-
-Variable A : Type.
-Variable Aequiv : A -> A -> Prop.
-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.
-
-Variable S : Setoid_Theory A Aequiv.
-
-Add Setoid A Aequiv S as Asetoid.
-
-Variable plus_morph :
- forall a a0:A, Aequiv a a0 ->
-   forall a1 a2:A, Aequiv a1 a2 ->
-     Aequiv (Aplus a a1)  (Aplus a0 a2).
-Variable mult_morph :
- forall a a0:A, Aequiv a a0 ->
-   forall a1 a2:A, Aequiv a1 a2 ->
-     Aequiv (Amult a a1) (Amult a0 a2).
-Variable opp_morph : forall a a0:A, Aequiv a a0 -> Aequiv (Aopp a) (Aopp a0).
-
-Add Morphism Aplus : Aplus_ext.
-intros; apply plus_morph; assumption.
-Qed.
-
-Add Morphism Amult : Amult_ext.
-intros; apply mult_morph; assumption.
-Qed.
-
-Add Morphism Aopp : Aopp_ext.
-exact opp_morph.
-Qed.
-
-Let equiv_refl := Seq_refl A Aequiv S.
-Let equiv_sym := Seq_sym A Aequiv S.
-Let equiv_trans := Seq_trans A Aequiv S.
-
-Hint Resolve equiv_refl equiv_trans.
-Hint Immediate equiv_sym.
-
-Section semi_setoid_rings.
-
-(* Section definitions. *)
-
-
-(******************************************)
-(* Normal abtract Polynomials             *)
-(******************************************)
-(* DEFINITIONS :
-- A varlist is a sorted product of one or more variables : x, x*y*z
-- A monom is a constant, a varlist or the product of a constant by a varlist
-  variables. 2*x*y, x*y*z, 3 are monoms : 2*3, x*3*y, 4*x*3 are NOT.
-- A canonical sum is either a monom or an ordered sum of monoms
-  (the order on monoms is defined later)
-- A normal polynomial it either a constant or a canonical sum or a constant
-  plus a canonical sum
-*)
-
-(* varlist is isomorphic to (list var), but we built a special inductive
-   for efficiency *)
-Inductive varlist : Type :=
-  | Nil_var : varlist
-  | Cons_var : index -> varlist -> varlist.
-
-Inductive canonical_sum : Type :=
-  | Nil_monom : canonical_sum
-  | Cons_monom : A -> varlist -> canonical_sum -> canonical_sum
-  | Cons_varlist : varlist -> canonical_sum -> canonical_sum.
-
-(* Order on monoms *)
-
-(* That's the lexicographic order on varlist, extended by :
-  - A constant is less than every monom
-  - The relation between two varlist is preserved by multiplication by a
-  constant.
-
-  Examples :
-  3 < x < y
-  x*y < x*y*y*z
-  2*x*y < x*y*y*z
-  x*y < 54*x*y*y*z
-  4*x*y < 59*x*y*y*z
-*)
-
-Fixpoint varlist_eq (x y:varlist) {struct y} : bool :=
-  match x, y with
-  | Nil_var, Nil_var => true
-  | Cons_var i xrest, Cons_var j yrest =>
-      andb (index_eq i j) (varlist_eq xrest yrest)
-  | _, _ => false
-  end.
-
-Fixpoint varlist_lt (x y:varlist) {struct y} : bool :=
-  match x, y with
-  | Nil_var, Cons_var _ _ => true
-  | Cons_var i xrest, Cons_var j yrest =>
-      if index_lt i j
-      then true
-      else andb (index_eq i j) (varlist_lt xrest yrest)
-  | _, _ => false
-  end.
-
-(* merges two variables lists *)
-Fixpoint varlist_merge (l1:varlist) : varlist -> varlist :=
-  match l1 with
-  | Cons_var v1 t1 =>
-      (fix vm_aux (l2:varlist) : varlist :=
-         match l2 with
-         | Cons_var v2 t2 =>
-             if index_lt v1 v2
-             then Cons_var v1 (varlist_merge t1 l2)
-             else Cons_var v2 (vm_aux t2)
-         | Nil_var => l1
-         end)
-  | Nil_var => fun l2 => l2
-  end.
-
-(* returns the sum of two canonical sums  *)
-Fixpoint canonical_sum_merge (s1:canonical_sum) :
- canonical_sum -> canonical_sum :=
-  match s1 with
-  | Cons_monom c1 l1 t1 =>
-      (fix csm_aux (s2:canonical_sum) : canonical_sum :=
-         match s2 with
-         | Cons_monom c2 l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus c1 c2) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
-              else Cons_monom c2 l2 (csm_aux t2)
-         | Cons_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus c1 Aone) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_monom c1 l1 (canonical_sum_merge t1 s2)
-              else Cons_varlist l2 (csm_aux t2)
-         | Nil_monom => s1
-         end)
-  | Cons_varlist l1 t1 =>
-      (fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
-         match s2 with
-         | Cons_monom c2 l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus Aone c2) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_varlist l1 (canonical_sum_merge t1 s2)
-              else Cons_monom c2 l2 (csm_aux2 t2)
-         | Cons_varlist l2 t2 =>
-             if varlist_eq l1 l2
-             then Cons_monom (Aplus Aone Aone) l1 (canonical_sum_merge t1 t2)
-             else
-              if varlist_lt l1 l2
-              then Cons_varlist l1 (canonical_sum_merge t1 s2)
-              else Cons_varlist l2 (csm_aux2 t2)
-         | Nil_monom => s1
-         end)
-  | Nil_monom => fun s2 => s2
-  end.
-
-(* Insertion of a monom in a canonical sum *)
-Fixpoint monom_insert (c1:A) (l1:varlist) (s2:canonical_sum) {struct s2} :
- canonical_sum :=
-  match s2 with
-  | Cons_monom c2 l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus c1 c2) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_monom c1 l1 s2
-       else Cons_monom c2 l2 (monom_insert c1 l1 t2)
-  | Cons_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus c1 Aone) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_monom c1 l1 s2
-       else Cons_varlist l2 (monom_insert c1 l1 t2)
-  | Nil_monom => Cons_monom c1 l1 Nil_monom
-  end.
-
-Fixpoint varlist_insert (l1:varlist) (s2:canonical_sum) {struct s2} :
- canonical_sum :=
-  match s2 with
-  | Cons_monom c2 l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus Aone c2) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_varlist l1 s2
-       else Cons_monom c2 l2 (varlist_insert l1 t2)
-  | Cons_varlist l2 t2 =>
-      if varlist_eq l1 l2
-      then Cons_monom (Aplus Aone Aone) l1 t2
-      else
-       if varlist_lt l1 l2
-       then Cons_varlist l1 s2
-       else Cons_varlist l2 (varlist_insert l1 t2)
-  | Nil_monom => Cons_varlist l1 Nil_monom
-  end.
-
-(* Computes c0*s *)
-Fixpoint canonical_sum_scalar (c0:A) (s:canonical_sum) {struct s} :
- canonical_sum :=
-  match s with
-  | Cons_monom c l t => Cons_monom (Amult c0 c) l (canonical_sum_scalar c0 t)
-  | Cons_varlist l t => Cons_monom c0 l (canonical_sum_scalar c0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* Computes l0*s  *)
-Fixpoint canonical_sum_scalar2 (l0:varlist) (s:canonical_sum) {struct s} :
- canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      monom_insert c (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
-  | Cons_varlist l t =>
-      varlist_insert (varlist_merge l0 l) (canonical_sum_scalar2 l0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* Computes c0*l0*s  *)
-Fixpoint canonical_sum_scalar3 (c0:A) (l0:varlist)
- (s:canonical_sum) {struct s} : canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      monom_insert (Amult c0 c) (varlist_merge l0 l)
-        (canonical_sum_scalar3 c0 l0 t)
-  | Cons_varlist l t =>
-      monom_insert c0 (varlist_merge l0 l) (canonical_sum_scalar3 c0 l0 t)
-  | Nil_monom => Nil_monom
-  end.
-
-(* returns the product of two canonical sums *)
-Fixpoint canonical_sum_prod (s1 s2:canonical_sum) {struct s1} :
- canonical_sum :=
-  match s1 with
-  | Cons_monom c1 l1 t1 =>
-      canonical_sum_merge (canonical_sum_scalar3 c1 l1 s2)
-        (canonical_sum_prod t1 s2)
-  | Cons_varlist l1 t1 =>
-      canonical_sum_merge (canonical_sum_scalar2 l1 s2)
-        (canonical_sum_prod t1 s2)
-  | Nil_monom => Nil_monom
-  end.
-
-(* The type to represent concrete semi-setoid-ring polynomials *)
-
-Inductive setspolynomial : Type :=
-  | SetSPvar : index -> setspolynomial
-  | SetSPconst : A -> setspolynomial
-  | SetSPplus : setspolynomial -> setspolynomial -> setspolynomial
-  | SetSPmult : setspolynomial -> setspolynomial -> setspolynomial.
-
-Fixpoint setspolynomial_normalize (p:setspolynomial) : canonical_sum :=
-  match p with
-  | SetSPplus l r =>
-      canonical_sum_merge (setspolynomial_normalize l)
-        (setspolynomial_normalize r)
-  | SetSPmult l r =>
-      canonical_sum_prod (setspolynomial_normalize l)
-        (setspolynomial_normalize r)
-  | SetSPconst c => Cons_monom c Nil_var Nil_monom
-  | SetSPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
-  end.
-
-Fixpoint canonical_sum_simplify (s:canonical_sum) : canonical_sum :=
-  match s with
-  | Cons_monom c l t =>
-      if Aeq c Azero
-      then canonical_sum_simplify t
-      else
-       if Aeq c Aone
-       then Cons_varlist l (canonical_sum_simplify t)
-       else Cons_monom c l (canonical_sum_simplify t)
-  | Cons_varlist l t => Cons_varlist l (canonical_sum_simplify t)
-  | Nil_monom => Nil_monom
-  end.
-
-Definition setspolynomial_simplify (x:setspolynomial) :=
-  canonical_sum_simplify (setspolynomial_normalize x).
-
-Variable vm : varmap A.
-
-Definition interp_var (i:index) := varmap_find Azero i vm.
-
-Definition ivl_aux :=
-  (fix ivl_aux (x:index) (t:varlist) {struct t} : A :=
-     match t with
-     | Nil_var => interp_var x
-     | Cons_var x' t' => Amult (interp_var x) (ivl_aux x' t')
-     end).
-
-Definition interp_vl (l:varlist) :=
-  match l with
-  | Nil_var => Aone
-  | Cons_var x t => ivl_aux x t
-  end.
-
-Definition interp_m (c:A) (l:varlist) :=
-  match l with
-  | Nil_var => c
-  | Cons_var x t => Amult c (ivl_aux x t)
-  end.
-
-Definition ics_aux :=
-  (fix ics_aux (a:A) (s:canonical_sum) {struct s} : A :=
-     match s with
-     | Nil_monom => a
-     | Cons_varlist l t => Aplus a (ics_aux (interp_vl l) t)
-     | Cons_monom c l t => Aplus a (ics_aux (interp_m c l) t)
-     end).
-
-Definition interp_setcs (s:canonical_sum) : A :=
-  match s with
-  | Nil_monom => Azero
-  | Cons_varlist l t => ics_aux (interp_vl l) t
-  | Cons_monom c l t => ics_aux (interp_m c l) t
-  end.
-
-Fixpoint interp_setsp (p:setspolynomial) : A :=
-  match p with
-  | SetSPconst c => c
-  | SetSPvar i => interp_var i
-  | SetSPplus p1 p2 => Aplus (interp_setsp p1) (interp_setsp p2)
-  | SetSPmult p1 p2 => Amult (interp_setsp p1) (interp_setsp p2)
-  end.
-
-(* End interpretation. *)
-
-Unset Implicit Arguments.
-
-(* Section properties. *)
-
-Variable T : Semi_Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aeq.
-
-Hint Resolve (SSR_plus_comm T).
-Hint Resolve (SSR_plus_assoc T).
-Hint Resolve (SSR_plus_assoc2 S T).
-Hint Resolve (SSR_mult_comm T).
-Hint Resolve (SSR_mult_assoc T).
-Hint Resolve (SSR_mult_assoc2 S T).
-Hint Resolve (SSR_plus_zero_left T).
-Hint Resolve (SSR_plus_zero_left2 S T).
-Hint Resolve (SSR_mult_one_left T).
-Hint Resolve (SSR_mult_one_left2 S T).
-Hint Resolve (SSR_mult_zero_left T).
-Hint Resolve (SSR_mult_zero_left2 S T).
-Hint Resolve (SSR_distr_left T).
-Hint Resolve (SSR_distr_left2 S T).
-Hint Resolve (SSR_plus_reg_left T).
-Hint Resolve (SSR_plus_permute S plus_morph T).
-Hint Resolve (SSR_mult_permute S mult_morph T).
-Hint Resolve (SSR_distr_right S plus_morph T).
-Hint Resolve (SSR_distr_right2 S plus_morph T).
-Hint Resolve (SSR_mult_zero_right S T).
-Hint Resolve (SSR_mult_zero_right2 S T).
-Hint Resolve (SSR_plus_zero_right S T).
-Hint Resolve (SSR_plus_zero_right2 S T).
-Hint Resolve (SSR_mult_one_right S T).
-Hint Resolve (SSR_mult_one_right2 S T).
-Hint Resolve (SSR_plus_reg_right S T).
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
-Proof.
-  simple induction x; simple induction y; contradiction || (try reflexivity).
-  simpl; intros.
-  generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
-  rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
-Qed.
-
-Remark ivl_aux_ok :
- forall (v:varlist) (i:index),
-   Aequiv (ivl_aux i v) (Amult (interp_var i) (interp_vl v)).
-Proof.
-  simple induction v; simpl; intros.
-  trivial.
-  rewrite (H i); trivial.
-Qed.
-
-Lemma varlist_merge_ok :
- forall x y:varlist,
-   Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)).
-Proof.
-  simple induction x.
-  simpl; trivial.
-  simple induction y.
-  simpl; trivial.
-  simpl; intros.
-  elim (index_lt i i0); simpl; intros.
-
-  rewrite (ivl_aux_ok v i).
-  rewrite (ivl_aux_ok v0 i0).
-  rewrite (ivl_aux_ok (varlist_merge v (Cons_var i0 v0)) i).
-  rewrite (H (Cons_var i0 v0)).
-  simpl.
-  rewrite (ivl_aux_ok v0 i0).
-  eauto.
-
-  rewrite (ivl_aux_ok v i).
-  rewrite (ivl_aux_ok v0 i0).
-  rewrite
-   (ivl_aux_ok
-      ((fix vm_aux (l2:varlist) : varlist :=
-          match l2 with
-          | Nil_var => Cons_var i v
-          | Cons_var v2 t2 =>
-              if index_lt i v2
-              then Cons_var i (varlist_merge v l2)
-              else Cons_var v2 (vm_aux t2)
-          end) v0) i0).
-  rewrite H0.
-  rewrite (ivl_aux_ok v i).
-  eauto.
-Qed.
-
-Remark ics_aux_ok :
- forall (x:A) (s:canonical_sum),
-   Aequiv (ics_aux x s) (Aplus x (interp_setcs s)).
-Proof.
- simple induction s; simpl; intros; trivial.
-Qed.
-
-Remark interp_m_ok :
- forall (x:A) (l:varlist), Aequiv (interp_m x l) (Amult x (interp_vl l)).
-Proof.
-  destruct l as [| i v]; trivial.
-Qed.
-
-Hint Resolve ivl_aux_ok.
-Hint Resolve ics_aux_ok.
-Hint Resolve interp_m_ok.
-
-(* Hints Resolve ivl_aux_ok ics_aux_ok interp_m_ok. *)
-
-Lemma canonical_sum_merge_ok :
- forall x y:canonical_sum,
-   Aequiv (interp_setcs (canonical_sum_merge x y))
-     (Aplus (interp_setcs x) (interp_setcs y)).
-Proof.
-simple induction x; simpl.
-trivial.
-
-simple induction y; simpl; intros.
-eauto.
-
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl.
-rewrite (ics_aux_ok (interp_m a v0) c).
-rewrite (ics_aux_ok (interp_m a0 v0) c0).
-rewrite (ics_aux_ok (interp_m (Aplus a a0) v0) (canonical_sum_merge c c0)).
-rewrite (H c0).
-rewrite (interp_m_ok (Aplus a a0) v0).
-rewrite (interp_m_ok a v0).
-rewrite (interp_m_ok a0 v0).
-setoid_replace (Amult (Aplus a a0) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult a (interp_vl v0)) (Amult a0 (interp_vl v0)))
-    (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult a (interp_vl v0))
-    (Aplus (Amult a0 (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
-    (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))) with
- (Aplus (Amult a (interp_vl v0))
-    (Aplus (interp_setcs c)
-       (Aplus (Amult a0 (interp_vl v0)) (interp_setcs c0))));
- [ idtac | trivial ].
-auto.
-
-elim (varlist_lt v v0); simpl.
-intro.
-rewrite
- (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_monom a0 v0 c0)))
- .
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (ics_aux_ok (interp_m a0 v0) c0).
-rewrite (H (Cons_monom a0 v0 c0)); simpl.
-rewrite (ics_aux_ok (interp_m a0 v0) c0); auto.
-
-intro.
-rewrite
- (ics_aux_ok (interp_m a0 v0)
-    ((fix csm_aux (s2:canonical_sum) : canonical_sum :=
-        match s2 with
-        | Nil_monom => Cons_monom a v c
-        | Cons_monom c2 l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_monom a v (canonical_sum_merge c s2)
-             else Cons_monom c2 l2 (csm_aux t2)
-        | Cons_varlist l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_monom a v (canonical_sum_merge c s2)
-             else Cons_varlist l2 (csm_aux t2)
-        end) c0)).
-rewrite H0.
-rewrite (ics_aux_ok (interp_m a v) c);
- rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl;
- auto.
-
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl.
-rewrite (ics_aux_ok (interp_m (Aplus a Aone) v0) (canonical_sum_merge c c0));
- rewrite (ics_aux_ok (interp_m a v0) c);
- rewrite (ics_aux_ok (interp_vl v0) c0).
-rewrite (H c0).
-rewrite (interp_m_ok (Aplus a Aone) v0).
-rewrite (interp_m_ok a v0).
-setoid_replace (Amult (Aplus a Aone) (interp_vl v0)) with
- (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult a (interp_vl v0)) (Amult Aone (interp_vl v0)))
-    (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult a (interp_vl v0))
-    (Aplus (Amult Aone (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult a (interp_vl v0)) (interp_setcs c))
-    (Aplus (interp_vl v0) (interp_setcs c0))) with
- (Aplus (Amult a (interp_vl v0))
-    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0);
- [ idtac | trivial ].
-auto.
-
-elim (varlist_lt v v0); simpl.
-intro.
-rewrite
- (ics_aux_ok (interp_m a v) (canonical_sum_merge c (Cons_varlist v0 c0)))
- ; rewrite (ics_aux_ok (interp_m a v) c);
- rewrite (ics_aux_ok (interp_vl v0) c0).
-rewrite (H (Cons_varlist v0 c0)); simpl.
-rewrite (ics_aux_ok (interp_vl v0) c0).
-auto.
-
-intro.
-rewrite
- (ics_aux_ok (interp_vl v0)
-    ((fix csm_aux (s2:canonical_sum) : canonical_sum :=
-        match s2 with
-        | Nil_monom => Cons_monom a v c
-        | Cons_monom c2 l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus a c2) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_monom a v (canonical_sum_merge c s2)
-             else Cons_monom c2 l2 (csm_aux t2)
-        | Cons_varlist l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus a Aone) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_monom a v (canonical_sum_merge c s2)
-             else Cons_varlist l2 (csm_aux t2)
-        end) c0)); rewrite H0.
-rewrite (ics_aux_ok (interp_m a v) c); rewrite (ics_aux_ok (interp_vl v0) c0);
- simpl.
-auto.
-
-simple induction y; simpl; intros.
-trivial.
-
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0).
-intros; rewrite (H1 I).
-simpl.
-rewrite (ics_aux_ok (interp_m (Aplus Aone a) v0) (canonical_sum_merge c c0));
- rewrite (ics_aux_ok (interp_vl v0) c);
- rewrite (ics_aux_ok (interp_m a v0) c0); rewrite (H c0).
-rewrite (interp_m_ok (Aplus Aone a) v0); rewrite (interp_m_ok a v0).
-setoid_replace (Amult (Aplus Aone a) (interp_vl v0)) with
- (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult a (interp_vl v0)))
-    (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult Aone (interp_vl v0))
-    (Aplus (Amult a (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (interp_vl v0) (interp_setcs c))
-    (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))) with
- (Aplus (interp_vl v0)
-    (Aplus (interp_setcs c)
-       (Aplus (Amult a (interp_vl v0)) (interp_setcs c0))));
- [ idtac | trivial ].
-auto.
-
-elim (varlist_lt v v0); simpl; intros.
-rewrite
- (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_monom a v0 c0)))
- ; rewrite (ics_aux_ok (interp_vl v) c);
- rewrite (ics_aux_ok (interp_m a v0) c0).
-rewrite (H (Cons_monom a v0 c0)); simpl.
-rewrite (ics_aux_ok (interp_m a v0) c0); auto.
-
-rewrite
- (ics_aux_ok (interp_m a v0)
-    ((fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
-        match s2 with
-        | Nil_monom => Cons_varlist v c
-        | Cons_monom c2 l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_varlist v (canonical_sum_merge c s2)
-             else Cons_monom c2 l2 (csm_aux2 t2)
-        | Cons_varlist l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_varlist v (canonical_sum_merge c s2)
-             else Cons_varlist l2 (csm_aux2 t2)
-        end) c0)); rewrite H0.
-rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_m a v0) c0);
- simpl; auto.
-
-generalize (varlist_eq_prop v v0).
-elim (varlist_eq v v0); intros.
-rewrite (H1 I); simpl.
-rewrite
- (ics_aux_ok (interp_m (Aplus Aone Aone) v0) (canonical_sum_merge c c0))
- ; rewrite (ics_aux_ok (interp_vl v0) c);
- rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H c0).
-rewrite (interp_m_ok (Aplus Aone Aone) v0).
-setoid_replace (Amult (Aplus Aone Aone) (interp_vl v0)) with
- (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (Amult Aone (interp_vl v0)) (Amult Aone (interp_vl v0)))
-    (Aplus (interp_setcs c) (interp_setcs c0))) with
- (Aplus (Amult Aone (interp_vl v0))
-    (Aplus (Amult Aone (interp_vl v0))
-       (Aplus (interp_setcs c) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace
- (Aplus (Aplus (interp_vl v0) (interp_setcs c))
-    (Aplus (interp_vl v0) (interp_setcs c0))) with
- (Aplus (interp_vl v0)
-    (Aplus (interp_setcs c) (Aplus (interp_vl v0) (interp_setcs c0))));
-[ idtac | trivial ].
-setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto.
-
-elim (varlist_lt v v0); simpl.
-rewrite
- (ics_aux_ok (interp_vl v) (canonical_sum_merge c (Cons_varlist v0 c0)))
- ; rewrite (ics_aux_ok (interp_vl v) c);
- rewrite (ics_aux_ok (interp_vl v0) c0); rewrite (H (Cons_varlist v0 c0));
- simpl.
-rewrite (ics_aux_ok (interp_vl v0) c0); auto.
-
-rewrite
- (ics_aux_ok (interp_vl v0)
-    ((fix csm_aux2 (s2:canonical_sum) : canonical_sum :=
-        match s2 with
-        | Nil_monom => Cons_varlist v c
-        | Cons_monom c2 l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus Aone c2) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_varlist v (canonical_sum_merge c s2)
-             else Cons_monom c2 l2 (csm_aux2 t2)
-        | Cons_varlist l2 t2 =>
-            if varlist_eq v l2
-            then Cons_monom (Aplus Aone Aone) v (canonical_sum_merge c t2)
-            else
-             if varlist_lt v l2
-             then Cons_varlist v (canonical_sum_merge c s2)
-             else Cons_varlist l2 (csm_aux2 t2)
-        end) c0)); rewrite H0.
-rewrite (ics_aux_ok (interp_vl v) c); rewrite (ics_aux_ok (interp_vl v0) c0);
- simpl; auto.
-Qed.
-
-Lemma monom_insert_ok :
- forall (a:A) (l:varlist) (s:canonical_sum),
-   Aequiv (interp_setcs (monom_insert a l s))
-     (Aplus (Amult a (interp_vl l)) (interp_setcs s)).
-Proof.
-simple induction s; intros.
-simpl; rewrite (interp_m_ok a l); trivial.
-
-simpl; generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl.
-rewrite (ics_aux_ok (interp_m (Aplus a a0) v) c);
- rewrite (ics_aux_ok (interp_m a0 v) c).
-rewrite (interp_m_ok (Aplus a a0) v); rewrite (interp_m_ok a0 v).
-setoid_replace (Amult (Aplus a a0) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult a0 (interp_vl v)));
- [ idtac | trivial ].
-auto.
-
-elim (varlist_lt l v); simpl; intros.
-rewrite (ics_aux_ok (interp_m a0 v) c).
-rewrite (interp_m_ok a0 v); rewrite (interp_m_ok a l).
-auto.
-
-rewrite (ics_aux_ok (interp_m a0 v) (monom_insert a l c));
- rewrite (ics_aux_ok (interp_m a0 v) c); rewrite H.
-auto.
-
-simpl.
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl.
-rewrite (ics_aux_ok (interp_m (Aplus a Aone) v) c);
- rewrite (ics_aux_ok (interp_vl v) c).
-rewrite (interp_m_ok (Aplus a Aone) v).
-setoid_replace (Amult (Aplus a Aone) (interp_vl v)) with
- (Aplus (Amult a (interp_vl v)) (Amult Aone (interp_vl v)));
- [ idtac | trivial ].
-setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v);
- [ idtac | trivial ].
-auto.
-
-elim (varlist_lt l v); simpl; intros; auto.
-rewrite (ics_aux_ok (interp_vl v) (monom_insert a l c)); rewrite H.
-rewrite (ics_aux_ok (interp_vl v) c); auto.
-Qed.
-
-Lemma varlist_insert_ok :
- forall (l:varlist) (s:canonical_sum),
-   Aequiv (interp_setcs (varlist_insert l s))
-     (Aplus (interp_vl l) (interp_setcs s)).
-Proof.
-simple induction s; simpl; intros.
-trivial.
-
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl.
-rewrite (ics_aux_ok (interp_m (Aplus Aone a) v) c);
- rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok (Aplus Aone a) v); rewrite (interp_m_ok a v).
-setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult a (interp_vl v)));
- [ idtac | trivial ].
-setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
-
-elim (varlist_lt l v); simpl; intros; auto.
-rewrite (ics_aux_ok (interp_m a v) (varlist_insert l c));
- rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok a v).
-rewrite H; auto.
-
-generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl.
-rewrite (ics_aux_ok (interp_m (Aplus Aone Aone) v) c);
- rewrite (ics_aux_ok (interp_vl v) c).
-rewrite (interp_m_ok (Aplus Aone Aone) v).
-setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with
- (Aplus (Amult Aone (interp_vl v)) (Amult Aone (interp_vl v)));
- [ idtac | trivial ].
-setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
-
-elim (varlist_lt l v); simpl; intros; auto.
-rewrite (ics_aux_ok (interp_vl v) (varlist_insert l c)).
-rewrite H.
-rewrite (ics_aux_ok (interp_vl v) c); auto.
-Qed.
-
-Lemma canonical_sum_scalar_ok :
- forall (a:A) (s:canonical_sum),
-   Aequiv (interp_setcs (canonical_sum_scalar a s))
-     (Amult a (interp_setcs s)).
-Proof.
-simple induction s; simpl; intros.
-trivial.
-
-rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c));
- rewrite (ics_aux_ok (interp_m a0 v) c).
-rewrite (interp_m_ok (Amult a a0) v); rewrite (interp_m_ok a0 v).
-rewrite H.
-setoid_replace (Amult a (Aplus (Amult a0 (interp_vl v)) (interp_setcs c)))
- with (Aplus (Amult a (Amult a0 (interp_vl v))) (Amult a (interp_setcs c)));
- [ idtac | trivial ].
-auto.
-
-rewrite (ics_aux_ok (interp_m a v) (canonical_sum_scalar a c));
- rewrite (ics_aux_ok (interp_vl v) c); rewrite H.
-rewrite (interp_m_ok a v).
-auto.
-Qed.
-
-Lemma canonical_sum_scalar2_ok :
- forall (l:varlist) (s:canonical_sum),
-   Aequiv (interp_setcs (canonical_sum_scalar2 l s))
-     (Amult (interp_vl l) (interp_setcs s)).
-Proof.
-simple induction s; simpl; intros; auto.
-rewrite (monom_insert_ok a (varlist_merge l v) (canonical_sum_scalar2 l c)).
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok a v).
-rewrite H.
-rewrite (varlist_merge_ok l v).
-setoid_replace
- (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c))) with
- (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-    (Amult (interp_vl l) (interp_setcs c)));
- [ idtac | trivial ].
-auto.
-
-rewrite (varlist_insert_ok (varlist_merge l v) (canonical_sum_scalar2 l c)).
-rewrite (ics_aux_ok (interp_vl v) c).
-rewrite H.
-rewrite (varlist_merge_ok l v).
-auto.
-Qed.
-
-Lemma canonical_sum_scalar3_ok :
- forall (c:A) (l:varlist) (s:canonical_sum),
-   Aequiv (interp_setcs (canonical_sum_scalar3 c l s))
-     (Amult c (Amult (interp_vl l) (interp_setcs s))).
-Proof.
-simple induction s; simpl; intros.
-rewrite (SSR_mult_zero_right S T (interp_vl l)).
-auto.
-
-rewrite
- (monom_insert_ok (Amult c a) (varlist_merge l v)
-    (canonical_sum_scalar3 c l c0)).
-rewrite (ics_aux_ok (interp_m a v) c0).
-rewrite (interp_m_ok a v).
-rewrite H.
-rewrite (varlist_merge_ok l v).
-setoid_replace
- (Amult (interp_vl l) (Aplus (Amult a (interp_vl v)) (interp_setcs c0))) with
- (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-    (Amult (interp_vl l) (interp_setcs c0)));
- [ idtac | trivial ].
-setoid_replace
- (Amult c
-    (Aplus (Amult (interp_vl l) (Amult a (interp_vl v)))
-       (Amult (interp_vl l) (interp_setcs c0)))) with
- (Aplus (Amult c (Amult (interp_vl l) (Amult a (interp_vl v))))
-    (Amult c (Amult (interp_vl l) (interp_setcs c0))));
- [ idtac | trivial ].
-setoid_replace (Amult (Amult c a) (Amult (interp_vl l) (interp_vl v))) with
- (Amult c (Amult a (Amult (interp_vl l) (interp_vl v))));
- [ idtac | trivial ].
-auto.
-
-rewrite
- (monom_insert_ok c (varlist_merge l v) (canonical_sum_scalar3 c l c0))
- .
-rewrite (ics_aux_ok (interp_vl v) c0).
-rewrite H.
-rewrite (varlist_merge_ok l v).
-setoid_replace
- (Aplus (Amult c (Amult (interp_vl l) (interp_vl v)))
-    (Amult c (Amult (interp_vl l) (interp_setcs c0)))) with
- (Amult c
-    (Aplus (Amult (interp_vl l) (interp_vl v))
-       (Amult (interp_vl l) (interp_setcs c0))));
- [ idtac | trivial ].
-auto.
-Qed.
-
-Lemma canonical_sum_prod_ok :
- forall x y:canonical_sum,
-   Aequiv (interp_setcs (canonical_sum_prod x y))
-     (Amult (interp_setcs x) (interp_setcs y)).
-Proof.
-simple induction x; simpl; intros.
-trivial.
-
-rewrite
- (canonical_sum_merge_ok (canonical_sum_scalar3 a v y)
-    (canonical_sum_prod c y)).
-rewrite (canonical_sum_scalar3_ok a v y).
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok a v).
-rewrite (H y).
-setoid_replace (Amult a (Amult (interp_vl v) (interp_setcs y))) with
- (Amult (Amult a (interp_vl v)) (interp_setcs y));
- [ idtac | trivial ].
-setoid_replace
- (Amult (Aplus (Amult a (interp_vl v)) (interp_setcs c)) (interp_setcs y))
- with
- (Aplus (Amult (Amult a (interp_vl v)) (interp_setcs y))
-    (Amult (interp_setcs c) (interp_setcs y)));
- [ idtac | trivial ].
-trivial.
-
-rewrite
- (canonical_sum_merge_ok (canonical_sum_scalar2 v y) (canonical_sum_prod c y))
- .
-rewrite (canonical_sum_scalar2_ok v y).
-rewrite (ics_aux_ok (interp_vl v) c).
-rewrite (H y).
-trivial.
-Qed.
-
-Theorem setspolynomial_normalize_ok :
- forall p:setspolynomial,
-   Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p).
-Proof.
-simple induction p; simpl; intros; trivial.
-rewrite
- (canonical_sum_merge_ok (setspolynomial_normalize s)
-    (setspolynomial_normalize s0)).
-rewrite H; rewrite H0; trivial.
-
-rewrite
- (canonical_sum_prod_ok (setspolynomial_normalize s)
-    (setspolynomial_normalize s0)).
-rewrite H; rewrite H0; trivial.
-Qed.
-
-Lemma canonical_sum_simplify_ok :
- forall s:canonical_sum,
-   Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s).
-Proof.
-simple induction s; simpl; intros.
-trivial.
-
-generalize (SSR_eq_prop T a Azero).
-elim (Aeq a Azero).
-simpl.
-intros.
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok a v).
-rewrite (H0 I).
-setoid_replace (Amult Azero (interp_vl v)) with Azero;
- [ idtac | trivial ].
-rewrite H.
-trivial.
-
-intros; simpl.
-generalize (SSR_eq_prop T a Aone).
-elim (Aeq a Aone).
-intros.
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite (interp_m_ok a v).
-rewrite (H1 I).
-simpl.
-rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
-rewrite H.
-auto.
-
-simpl.
-intros.
-rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)).
-rewrite (ics_aux_ok (interp_m a v) c).
-rewrite H; trivial.
-
-rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
-rewrite H.
-auto.
-Qed.
-
-Theorem setspolynomial_simplify_ok :
- forall p:setspolynomial,
-   Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p).
-Proof.
-intro.
-unfold setspolynomial_simplify.
-rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)).
-exact (setspolynomial_normalize_ok p).
-Qed.
-
-End semi_setoid_rings.
-
-Arguments Cons_varlist : default implicits.
-Arguments Cons_monom : default implicits.
-Arguments SetSPconst : default implicits.
-Arguments SetSPplus : default implicits.
-Arguments SetSPmult : default implicits.
-
-
-
-Section setoid_rings.
-
-Set Implicit Arguments.
-
-Variable vm : varmap A.
-Variable T : Setoid_Ring_Theory Aequiv Aplus Amult Aone Azero Aopp Aeq.
-
-Hint Resolve (STh_plus_comm T).
-Hint Resolve (STh_plus_assoc T).
-Hint Resolve (STh_plus_assoc2 S T).
-Hint Resolve (STh_mult_comm T).
-Hint Resolve (STh_mult_assoc T).
-Hint Resolve (STh_mult_assoc2 S T).
-Hint Resolve (STh_plus_zero_left T).
-Hint Resolve (STh_plus_zero_left2 S T).
-Hint Resolve (STh_mult_one_left T).
-Hint Resolve (STh_mult_one_left2 S T).
-Hint Resolve (STh_mult_zero_left S plus_morph mult_morph T).
-Hint Resolve (STh_mult_zero_left2 S plus_morph mult_morph T).
-Hint Resolve (STh_distr_left T).
-Hint Resolve (STh_distr_left2 S T).
-Hint Resolve (STh_plus_reg_left S plus_morph T).
-Hint Resolve (STh_plus_permute S plus_morph T).
-Hint Resolve (STh_mult_permute S mult_morph T).
-Hint Resolve (STh_distr_right S plus_morph T).
-Hint Resolve (STh_distr_right2 S plus_morph T).
-Hint Resolve (STh_mult_zero_right S plus_morph mult_morph T).
-Hint Resolve (STh_mult_zero_right2 S plus_morph mult_morph T).
-Hint Resolve (STh_plus_zero_right S T).
-Hint Resolve (STh_plus_zero_right2 S T).
-Hint Resolve (STh_mult_one_right S T).
-Hint Resolve (STh_mult_one_right2 S T).
-Hint Resolve (STh_plus_reg_right S plus_morph T).
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-
-(*** Definitions *)
-
-Inductive setpolynomial : Type :=
-  | SetPvar : index -> setpolynomial
-  | SetPconst : A -> setpolynomial
-  | SetPplus : setpolynomial -> setpolynomial -> setpolynomial
-  | SetPmult : setpolynomial -> setpolynomial -> setpolynomial
-  | SetPopp : setpolynomial -> setpolynomial.
-
-Fixpoint setpolynomial_normalize (x:setpolynomial) : canonical_sum :=
-  match x with
-  | SetPplus l r =>
-      canonical_sum_merge (setpolynomial_normalize l)
-        (setpolynomial_normalize r)
-  | SetPmult l r =>
-      canonical_sum_prod (setpolynomial_normalize l)
-        (setpolynomial_normalize r)
-  | SetPconst c => Cons_monom c Nil_var Nil_monom
-  | SetPvar i => Cons_varlist (Cons_var i Nil_var) Nil_monom
-  | SetPopp p =>
-      canonical_sum_scalar3 (Aopp Aone) Nil_var (setpolynomial_normalize p)
-  end.
-
-Definition setpolynomial_simplify (x:setpolynomial) :=
-  canonical_sum_simplify (setpolynomial_normalize x).
-
-Fixpoint setspolynomial_of (x:setpolynomial) : setspolynomial :=
-  match x with
-  | SetPplus l r => SetSPplus (setspolynomial_of l) (setspolynomial_of r)
-  | SetPmult l r => SetSPmult (setspolynomial_of l) (setspolynomial_of r)
-  | SetPconst c => SetSPconst c
-  | SetPvar i => SetSPvar i
-  | SetPopp p => SetSPmult (SetSPconst (Aopp Aone)) (setspolynomial_of p)
-  end.
-
-(*** Interpretation *)
-
-Fixpoint interp_setp (p:setpolynomial) : A :=
-  match p with
-  | SetPconst c => c
-  | SetPvar i => varmap_find Azero i vm
-  | SetPplus p1 p2 => Aplus (interp_setp p1) (interp_setp p2)
-  | SetPmult p1 p2 => Amult (interp_setp p1) (interp_setp p2)
-  | SetPopp p1 => Aopp (interp_setp p1)
-  end.
-
-(*** Properties *)
-
-Unset Implicit Arguments.
-
-Lemma setspolynomial_of_ok :
- forall p:setpolynomial,
-   Aequiv (interp_setp p) (interp_setsp vm (setspolynomial_of p)).
-simple induction p; trivial; simpl; intros.
-rewrite H; rewrite H0; trivial.
-rewrite H; rewrite H0; trivial.
-rewrite H.
-rewrite
- (STh_opp_mult_left2 S plus_morph mult_morph T Aone
-    (interp_setsp vm (setspolynomial_of s))).
-rewrite (STh_mult_one_left T (interp_setsp vm (setspolynomial_of s))).
-trivial.
-Qed.
-
-Theorem setpolynomial_normalize_ok :
- forall p:setpolynomial,
-   setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p).
-simple induction p; trivial; simpl; intros.
-rewrite H; rewrite H0; reflexivity.
-rewrite H; rewrite H0; reflexivity.
-rewrite H; simpl.
-elim
- (canonical_sum_scalar3 (Aopp Aone) Nil_var
-    (setspolynomial_normalize (setspolynomial_of s)));
- [ reflexivity
- | simpl; intros; rewrite H0; reflexivity
- | simpl; intros; rewrite H0; reflexivity ].
-Qed.
-
-Theorem setpolynomial_simplify_ok :
- forall p:setpolynomial,
-   Aequiv (interp_setcs vm (setpolynomial_simplify p)) (interp_setp p).
-intro.
-unfold setpolynomial_simplify.
-rewrite (setspolynomial_of_ok p).
-rewrite setpolynomial_normalize_ok.
-rewrite
- (canonical_sum_simplify_ok vm
-    (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq
-       plus_morph mult_morph T)
-    (setspolynomial_normalize (setspolynomial_of p)))
- .
-rewrite
- (setspolynomial_normalize_ok vm
-    (Semi_Setoid_Ring_Theory_of A Aequiv S Aplus Amult Aone Azero Aopp Aeq
-       plus_morph mult_morph T) (setspolynomial_of p))
- .
-trivial.
-Qed.
-
-End setoid_rings.
-
-End setoid.
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
deleted file mode 100644
index 870fe40f1..000000000
--- a/plugins/ring/Setoid_ring_theory.v
+++ /dev/null
@@ -1,425 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Bool.
-Require Export Setoid.
-
-Set Implicit Arguments.
-
-Section Setoid_rings.
-
-Variable A : Type.
-Variable Aequiv : A -> A -> Prop.
-
-Infix Local "==" := Aequiv (at level 70, no associativity).
-
-Variable S : Setoid_Theory A Aequiv.
-
-Add Setoid A Aequiv S as Asetoid.
-
-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.
-
-Infix "+" := Aplus (at level 50, left associativity).
-Infix "*" := Amult (at level 40, left associativity).
-Notation "0" := Azero.
-Notation "1" := Aone.
-Notation "- x" := (Aopp x).
-
-Variable plus_morph :
- forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a + a1 == a0 + a2.
-Variable mult_morph :
-  forall a a0:A, a == a0 -> forall a1 a2:A, a1 == a2 -> a * a1 == a0 * a2.
-Variable opp_morph : forall a a0:A, a == a0 -> - a == - a0.
-
-Add Morphism Aplus : Aplus_ext.
-intros; apply plus_morph; assumption.
-Qed.
-
-Add Morphism Amult : Amult_ext.
-intros; apply mult_morph; assumption.
-Qed.
-
-Add Morphism Aopp : Aopp_ext.
-exact opp_morph.
-Qed.
-
-Section Theory_of_semi_setoid_rings.
-
-Record Semi_Setoid_Ring_Theory : Prop :=
-  {SSR_plus_comm : forall n m:A, n + m == m + n;
-   SSR_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
-   SSR_mult_comm : forall n m:A, n * m == m * n;
-   SSR_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
-   SSR_plus_zero_left : forall n:A, 0 + n == n;
-   SSR_mult_one_left : forall n:A, 1 * n == n;
-   SSR_mult_zero_left : forall n:A, 0 * n == 0;
-   SSR_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
-   SSR_plus_reg_left : forall n m p:A, n + m == n + p -> m == p;
-   SSR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.
-
-Variable T : Semi_Setoid_Ring_Theory.
-
-Let plus_comm := SSR_plus_comm T.
-Let plus_assoc := SSR_plus_assoc T.
-Let mult_comm := SSR_mult_comm T.
-Let mult_assoc := SSR_mult_assoc T.
-Let plus_zero_left := SSR_plus_zero_left T.
-Let mult_one_left := SSR_mult_one_left T.
-Let mult_zero_left := SSR_mult_zero_left T.
-Let distr_left := SSR_distr_left T.
-Let plus_reg_left := SSR_plus_reg_left T.
-Let equiv_refl := Seq_refl A Aequiv S.
-Let equiv_sym := Seq_sym A Aequiv S.
-Let equiv_trans := Seq_trans A Aequiv S.
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left mult_zero_left distr_left plus_reg_left
-  equiv_refl (*equiv_sym*).
-Hint Immediate equiv_sym.
-
-(* Lemmas whose form is x=y are also provided in form y=x because
-  Auto does not symmetry *)
-Lemma SSR_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).
-auto. Qed.
-
-Lemma SSR_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).
-auto. Qed.
-
-Lemma SSR_plus_zero_left2 : forall n:A, n == 0 + n.
-auto. Qed.
-
-Lemma SSR_mult_one_left2 : forall n:A, n == 1 * n.
-auto. Qed.
-
-Lemma SSR_mult_zero_left2 : forall n:A, 0 == 0 * n.
-auto. Qed.
-
-Lemma SSR_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.
-auto. Qed.
-
-Lemma SSR_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).
-intros.
-rewrite (plus_assoc n m p).
-rewrite (plus_comm n m).
-rewrite <- (plus_assoc m n p).
-trivial.
-Qed.
-
-Lemma SSR_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).
-intros.
-rewrite (mult_assoc n m p).
-rewrite (mult_comm n m).
-rewrite <- (mult_assoc m n p).
-trivial.
-Qed.
-
-Hint Resolve SSR_plus_permute SSR_mult_permute.
-
-Lemma SSR_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.
-intros.
-rewrite (mult_comm n (m + p)).
-rewrite (mult_comm n m).
-rewrite (mult_comm n p).
-auto.
-Qed.
-
-Lemma SSR_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).
-intros.
-apply equiv_sym.
-apply SSR_distr_right.
-Qed.
-
-Lemma SSR_mult_zero_right : forall n:A, n * 0 == 0.
-intro; rewrite (mult_comm n 0); auto.
-Qed.
-
-Lemma SSR_mult_zero_right2 : forall n:A, 0 == n * 0.
-intro; rewrite (mult_comm n 0); auto.
-Qed.
-
-Lemma SSR_plus_zero_right : forall n:A, n + 0 == n.
-intro; rewrite (plus_comm n 0); auto.
-Qed.
-
-Lemma SSR_plus_zero_right2 : forall n:A, n == n + 0.
-intro; rewrite (plus_comm n 0); auto.
-Qed.
-
-Lemma SSR_mult_one_right : forall n:A, n * 1 == n.
-intro; rewrite (mult_comm n 1); auto.
-Qed.
-
-Lemma SSR_mult_one_right2 : forall n:A, n == n * 1.
-intro; rewrite (mult_comm n 1); auto.
-Qed.
-
-Lemma SSR_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.
-intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n).
-intro; apply plus_reg_left with n; trivial.
-Qed.
-
-End Theory_of_semi_setoid_rings.
-
-Section Theory_of_setoid_rings.
-
-Record Setoid_Ring_Theory : Prop :=
-  {STh_plus_comm : forall n m:A, n + m == m + n;
-   STh_plus_assoc : forall n m p:A, n + (m + p) == n + m + p;
-   STh_mult_comm : forall n m:A, n * m == m * n;
-   STh_mult_assoc : forall n m p:A, n * (m * p) == n * m * p;
-   STh_plus_zero_left : forall n:A, 0 + n == n;
-   STh_mult_one_left : forall n:A, 1 * n == n;
-   STh_opp_def : forall n:A, n + - n == 0;
-   STh_distr_left : forall n m p:A, (n + m) * p == n * p + m * p;
-   STh_eq_prop : forall x y:A, Is_true (Aeq x y) -> x == y}.
-
-Variable T : Setoid_Ring_Theory.
-
-Let plus_comm := STh_plus_comm T.
-Let plus_assoc := STh_plus_assoc T.
-Let mult_comm := STh_mult_comm T.
-Let mult_assoc := STh_mult_assoc T.
-Let plus_zero_left := STh_plus_zero_left T.
-Let mult_one_left := STh_mult_one_left T.
-Let opp_def := STh_opp_def T.
-Let distr_left := STh_distr_left T.
-Let equiv_refl := Seq_refl A Aequiv S.
-Let equiv_sym := Seq_sym A Aequiv S.
-Let equiv_trans := Seq_trans A Aequiv S.
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
-  mult_one_left opp_def distr_left equiv_refl equiv_sym.
-
-(* Lemmas whose form is x=y are also provided in form y=x because Auto does
-  not symmetry *)
-
-Lemma STh_mult_assoc2 : forall n m p:A, n * m * p == n * (m * p).
-auto. Qed.
-
-Lemma STh_plus_assoc2 : forall n m p:A, n + m + p == n + (m + p).
-auto. Qed.
-
-Lemma STh_plus_zero_left2 : forall n:A, n == 0 + n.
-auto. Qed.
-
-Lemma STh_mult_one_left2 : forall n:A, n == 1 * n.
-auto. Qed.
-
-Lemma STh_distr_left2 : forall n m p:A, n * p + m * p == (n + m) * p.
-auto. Qed.
-
-Lemma STh_opp_def2 : forall n:A, 0 == n + - n.
-auto. Qed.
-
-Lemma STh_plus_permute : forall n m p:A, n + (m + p) == m + (n + p).
-intros.
-rewrite (plus_assoc n m p).
-rewrite (plus_comm n m).
-rewrite <- (plus_assoc m n p).
-trivial.
-Qed.
-
-Lemma STh_mult_permute : forall n m p:A, n * (m * p) == m * (n * p).
-intros.
-rewrite (mult_assoc n m p).
-rewrite (mult_comm n m).
-rewrite <- (mult_assoc m n p).
-trivial.
-Qed.
-
-Hint Resolve STh_plus_permute STh_mult_permute.
-
-Lemma Saux1 : forall a:A, a + a == a -> a == 0.
-intros.
-rewrite <- (plus_zero_left a).
-rewrite (plus_comm 0 a).
-setoid_replace (a + 0) with (a + (a + - a)) by auto.
-rewrite (plus_assoc a a (- a)).
-rewrite H.
-apply opp_def.
-Qed.
-
-Lemma STh_mult_zero_left : forall n:A, 0 * n == 0.
-intros.
-apply Saux1.
-rewrite <- (distr_left 0 0 n).
-rewrite (plus_zero_left 0).
-trivial.
-Qed.
-Hint Resolve STh_mult_zero_left.
-
-Lemma STh_mult_zero_left2 : forall n:A, 0 == 0 * n.
-auto.
-Qed.
-
-Lemma Saux2 : forall x y z:A, x + y == 0 -> x + z == 0 -> y == z.
-intros.
-rewrite <- (plus_zero_left y).
-rewrite <- H0.
-rewrite <- (plus_assoc x z y).
-rewrite (plus_comm z y).
-rewrite (plus_assoc x y z).
-rewrite H.
-auto.
-Qed.
-
-Lemma STh_opp_mult_left : forall x y:A, - (x * y) == - x * y.
-intros.
-apply Saux2 with (x * y); auto.
-rewrite <- (distr_left x (- x) y).
-rewrite (opp_def x).
-auto.
-Qed.
-Hint Resolve STh_opp_mult_left.
-
-Lemma STh_opp_mult_left2 : forall x y:A, - x * y == - (x * y).
-auto.
-Qed.
-
-Lemma STh_mult_zero_right : forall n:A, n * 0 == 0.
-intro; rewrite (mult_comm n 0); auto.
-Qed.
-
-Lemma STh_mult_zero_right2 : forall n:A, 0 == n * 0.
-intro; rewrite (mult_comm n 0); auto.
-Qed.
-
-Lemma STh_plus_zero_right : forall n:A, n + 0 == n.
-intro; rewrite (plus_comm n 0); auto.
-Qed.
-
-Lemma STh_plus_zero_right2 : forall n:A, n == n + 0.
-intro; rewrite (plus_comm n 0); auto.
-Qed.
-
-Lemma STh_mult_one_right : forall n:A, n * 1 == n.
-intro; rewrite (mult_comm n 1); auto.
-Qed.
-
-Lemma STh_mult_one_right2 : forall n:A, n == n * 1.
-intro; rewrite (mult_comm n 1); auto.
-Qed.
-
-Lemma STh_opp_mult_right : forall x y:A, - (x * y) == x * - y.
-intros.
-rewrite (mult_comm x y).
-rewrite (mult_comm x (- y)).
-auto.
-Qed.
-
-Lemma STh_opp_mult_right2 : forall x y:A, x * - y == - (x * y).
-intros.
-rewrite (mult_comm x y).
-rewrite (mult_comm x (- y)).
-auto.
-Qed.
-
-Lemma STh_plus_opp_opp : forall x y:A, - x + - y == - (x + y).
-intros.
-apply Saux2 with (x + y); auto.
-rewrite (STh_plus_permute (x + y) (- x) (- y)).
-rewrite <- (plus_assoc x y (- y)).
-rewrite (opp_def y); rewrite (STh_plus_zero_right x).
-rewrite (STh_opp_def2 x); trivial.
-Qed.
-
-Lemma STh_plus_permute_opp : forall n m p:A, - m + (n + p) == n + (- m + p).
-auto.
-Qed.
-
-Lemma STh_opp_opp : forall n:A, - - n == n.
-intro.
-apply Saux2 with (- n); auto.
-rewrite (plus_comm (- n) n); auto.
-Qed.
-Hint Resolve STh_opp_opp.
-
-Lemma STh_opp_opp2 : forall n:A, n == - - n.
-auto.
-Qed.
-
-Lemma STh_mult_opp_opp : forall x y:A, - x * - y == x * y.
-intros.
-rewrite (STh_opp_mult_left2 x (- y)).
-rewrite (STh_opp_mult_right2 x y).
-trivial.
-Qed.
-
-Lemma STh_mult_opp_opp2 : forall x y:A, x * y == - x * - y.
-intros.
-apply equiv_sym.
-apply STh_mult_opp_opp.
-Qed.
-
-Lemma STh_opp_zero : - 0 == 0.
-rewrite <- (plus_zero_left (- 0)).
-trivial.
-Qed.
-
-Lemma STh_plus_reg_left : forall n m p:A, n + m == n + p -> m == p.
-intros.
-rewrite <- (plus_zero_left m).
-rewrite <- (plus_zero_left p).
-rewrite <- (opp_def n).
-rewrite (plus_comm n (- n)).
-rewrite <- (plus_assoc (- n) n m).
-rewrite <- (plus_assoc (- n) n p).
-auto.
-Qed.
-
-Lemma STh_plus_reg_right : forall n m p:A, m + n == p + n -> m == p.
-intros.
-apply STh_plus_reg_left with n.
-rewrite (plus_comm n m); rewrite (plus_comm n p); assumption.
-Qed.
-
-Lemma STh_distr_right : forall n m p:A, n * (m + p) == n * m + n * p.
-intros.
-rewrite (mult_comm n (m + p)).
-rewrite (mult_comm n m).
-rewrite (mult_comm n p).
-trivial.
-Qed.
-
-Lemma STh_distr_right2 : forall n m p:A, n * m + n * p == n * (m + p).
-intros.
-apply equiv_sym.
-apply STh_distr_right.
-Qed.
-
-End Theory_of_setoid_rings.
-
-Hint Resolve STh_mult_zero_left STh_plus_reg_left: core.
-
-Unset Implicit Arguments.
-
-Definition Semi_Setoid_Ring_Theory_of :
-  Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
-intros until 1; case H.
-split; intros; simpl; eauto.
-Defined.
-
-Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >->
- Semi_Setoid_Ring_Theory.
-
-
-
-Section product_ring.
-
-End product_ring.
-
-Section power_ring.
-
-End power_ring.
-
-End Setoid_rings.
diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
deleted file mode 100644
index 758de80ba..000000000
--- a/plugins/ring/g_ring.ml4
+++ /dev/null
@@ -1,134 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Quote
-open Ring
-open Tacticals
-
-TACTIC EXTEND ring
-| [ "legacy" "ring" constr_list(l) ] -> [ polynom l ]
-END
-
-(* The vernac commands "Add Ring" and co *)
-
-let cset_of_constrarg_list l =
-  List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
-
-VERNAC COMMAND EXTEND AddRing
-  [ "Add" "Legacy" "Ring"
-          constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
-          constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ]
-  -> [ add_theory true false false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_constrarg_list l) ]
-
-| [ "Add" "Legacy" "Semi" "Ring"
-      	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
-          constr(aeq) constr(t) "[" ne_constr_list(l) "]" ]
-  -> [ add_theory false false false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_constrarg_list l) ]
-
-| [ "Add" "Legacy" "Abstract" "Ring"
-    	  constr(a) constr(aplus) constr(amult) constr(aone)
-          constr(azero) constr(aopp) constr(aeq) constr(t) ]
-  -> [ add_theory true true false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 ConstrSet.empty ]
-
-| [ "Add" "Legacy" "Abstract" "Semi" "Ring"
-          constr(a) constr(aplus) constr(amult) constr(aone)
-          constr(azero) constr(aeq) constr(t) ]
-  -> [ add_theory false true false
-			 (constr_of a)
-			 None
-			 None
-			 None
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 ConstrSet.empty ]
-
-| [ "Add" "Legacy" "Setoid" "Ring"
-      	  constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult)
-	  constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
-	  constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ]
-  -> [ add_theory true false true
-			 (constr_of a)
-			 (Some (constr_of aequiv))
-			 (Some (constr_of asetth))
-			 (Some {
-			    plusm = (constr_of pm);
-			    multm = (constr_of mm);
-			    oppm = Some (constr_of om) })
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 (Some (constr_of aopp))
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_constrarg_list l) ]
-
-| [ "Add" "Legacy" "Semi" "Setoid" "Ring"
-          constr(a) constr(aequiv) constr(asetth) constr(aplus)
-	  constr(amult) constr(aone) constr(azero) constr(aeq)
-          constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ]
-  -> [ add_theory false false true
-			 (constr_of a)
-			 (Some (constr_of aequiv))
-			 (Some (constr_of asetth))
-			 (Some {
-			    plusm = (constr_of pm);
-			    multm = (constr_of mm);
-			    oppm = None })
-			 (constr_of aplus)
-			 (constr_of amult)
-			 (constr_of aone)
-			 (constr_of azero)
-			 None
-			 (constr_of aeq)
-			 (constr_of t)
-			 (cset_of_constrarg_list l) ]
-END
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
deleted file mode 100644
index 22d5adb18..000000000
--- a/plugins/ring/ring.ml
+++ /dev/null
@@ -1,929 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* ML part of the Ring tactic *)
-
-open Pp
-open Errors
-open Util
-open Flags
-open Term
-open Names
-open Libnames
-open Globnames
-open Nameops
-open Reductionops
-open Tacticals
-open Tacexpr
-open Tacmach
-open Printer
-open Equality
-open Vernacinterp
-open Vernacexpr
-open Libobject
-open Closure
-open Tacred
-open Tactics
-open Pattern
-open Hiddentac
-open Nametab
-open Quote
-open Mod_subst
-
-let mt_evd = Evd.empty
-let constr_of c = Constrintern.interp_constr mt_evd (Global.env()) c
-
-let ring_dir = ["Coq";"ring"]
-let setoids_dir = ["Coq";"Setoids"]
-
-let ring_constant = Coqlib.gen_constant_in_modules "Ring"
-  [ring_dir@["LegacyRing_theory"];
-   ring_dir@["Setoid_ring_theory"];
-   ring_dir@["Ring_normalize"];
-   ring_dir@["Ring_abstract"];
-   setoids_dir@["Setoid"];
-   ring_dir@["Setoid_ring_normalize"]]
-
-(* Ring theory *)
-let coq_Ring_Theory = lazy (ring_constant "Ring_Theory")
-let coq_Semi_Ring_Theory = lazy (ring_constant "Semi_Ring_Theory")
-
-(* Setoid ring theory *)
-let coq_Setoid_Ring_Theory = lazy (ring_constant "Setoid_Ring_Theory")
-let coq_Semi_Setoid_Ring_Theory = lazy(ring_constant "Semi_Setoid_Ring_Theory")
-
-(* Ring normalize *)
-let coq_SPplus = lazy (ring_constant "SPplus")
-let coq_SPmult = lazy (ring_constant "SPmult")
-let coq_SPvar = lazy (ring_constant "SPvar")
-let coq_SPconst = lazy (ring_constant "SPconst")
-let coq_Pplus = lazy (ring_constant "Pplus")
-let coq_Pmult = lazy (ring_constant "Pmult")
-let coq_Pvar = lazy (ring_constant "Pvar")
-let coq_Pconst = lazy (ring_constant "Pconst")
-let coq_Popp = lazy (ring_constant "Popp")
-let coq_interp_sp = lazy (ring_constant "interp_sp")
-let coq_interp_p = lazy (ring_constant "interp_p")
-let coq_interp_cs = lazy (ring_constant "interp_cs")
-let coq_spolynomial_simplify = lazy (ring_constant "spolynomial_simplify")
-let coq_polynomial_simplify = lazy (ring_constant "polynomial_simplify")
-let coq_spolynomial_simplify_ok = lazy(ring_constant "spolynomial_simplify_ok")
-let coq_polynomial_simplify_ok = lazy (ring_constant "polynomial_simplify_ok")
-
-(* Setoid theory *)
-let coq_Setoid_Theory = lazy(ring_constant "Setoid_Theory")
-
-let coq_seq_refl = lazy(ring_constant "Seq_refl")
-let coq_seq_sym = lazy(ring_constant "Seq_sym")
-let coq_seq_trans = lazy(ring_constant "Seq_trans")
-
-(* Setoid Ring normalize *)
-let coq_SetSPplus = lazy (ring_constant "SetSPplus")
-let coq_SetSPmult = lazy (ring_constant "SetSPmult")
-let coq_SetSPvar = lazy (ring_constant "SetSPvar")
-let coq_SetSPconst = lazy (ring_constant "SetSPconst")
-let coq_SetPplus = lazy (ring_constant "SetPplus")
-let coq_SetPmult = lazy (ring_constant "SetPmult")
-let coq_SetPvar = lazy (ring_constant "SetPvar")
-let coq_SetPconst = lazy (ring_constant "SetPconst")
-let coq_SetPopp = lazy (ring_constant "SetPopp")
-let coq_interp_setsp = lazy (ring_constant "interp_setsp")
-let coq_interp_setp = lazy (ring_constant "interp_setp")
-let coq_interp_setcs = lazy (ring_constant "interp_setcs")
-let coq_setspolynomial_simplify =
-  lazy (ring_constant "setspolynomial_simplify")
-let coq_setpolynomial_simplify =
-  lazy (ring_constant "setpolynomial_simplify")
-let coq_setspolynomial_simplify_ok =
-  lazy (ring_constant "setspolynomial_simplify_ok")
-let coq_setpolynomial_simplify_ok =
-  lazy (ring_constant "setpolynomial_simplify_ok")
-
-(* Ring abstract *)
-let coq_ASPplus = lazy (ring_constant "ASPplus")
-let coq_ASPmult = lazy (ring_constant "ASPmult")
-let coq_ASPvar = lazy (ring_constant "ASPvar")
-let coq_ASP0 = lazy (ring_constant "ASP0")
-let coq_ASP1 = lazy (ring_constant "ASP1")
-let coq_APplus = lazy (ring_constant "APplus")
-let coq_APmult = lazy (ring_constant "APmult")
-let coq_APvar = lazy (ring_constant "APvar")
-let coq_AP0 = lazy (ring_constant "AP0")
-let coq_AP1 = lazy (ring_constant "AP1")
-let coq_APopp = lazy (ring_constant "APopp")
-let coq_interp_asp = lazy (ring_constant "interp_asp")
-let coq_interp_ap = lazy (ring_constant "interp_ap")
-let coq_interp_acs = lazy (ring_constant "interp_acs")
-let coq_interp_sacs = lazy (ring_constant "interp_sacs")
-let coq_aspolynomial_normalize = lazy (ring_constant "aspolynomial_normalize")
-let coq_apolynomial_normalize = lazy (ring_constant "apolynomial_normalize")
-let coq_aspolynomial_normalize_ok =
-  lazy (ring_constant "aspolynomial_normalize_ok")
-let coq_apolynomial_normalize_ok =
-  lazy (ring_constant "apolynomial_normalize_ok")
-
-(* Logic --> to be found in Coqlib *)
-open Coqlib
-
-let mkLApp(fc,v) = mkApp(Lazy.force fc, v)
-
-(*********** Useful types and functions ************)
-
-module OperSet =
-  Set.Make (struct
-	      type t = global_reference
-	      let compare = (RefOrdered.compare : t->t->int)
-	    end)
-
-type morph =
-    { plusm : constr;
-      multm : constr;
-      oppm : constr option;
-    }
-
-type theory =
-    { th_ring : bool;                  (* false for a semi-ring *)
-      th_abstract : bool;
-      th_setoid : bool;                (* true for a setoid ring *)
-      th_equiv : constr option;
-      th_setoid_th : constr option;
-      th_morph : morph option;
-      th_a : constr;                   (* e.g. nat *)
-      th_plus : constr;
-      th_mult : constr;
-      th_one : constr;
-      th_zero : constr;
-      th_opp : constr option;          (* None if semi-ring *)
-      th_eq : constr;
-      th_t : constr;                   (* e.g. NatTheory *)
-      th_closed : ConstrSet.t;         (* e.g. [S; O] *)
-                                       (* Must be empty for an abstract ring *)
-    }
-
-(* Theories are stored in a table which is synchronised with the Reset
-   mechanism. *)
-
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
-
-let theories_map = ref Cmap.empty
-
-let theories_map_add (c,t) = theories_map := Cmap.add c t !theories_map
-let theories_map_find c = Cmap.find c !theories_map
-let theories_map_mem c = Cmap.mem c !theories_map
-
-let _ =
-  Summary.declare_summary "tactic-ring-table"
-    { Summary.freeze_function = (fun () -> !theories_map);
-      Summary.unfreeze_function = (fun t -> theories_map := t);
-      Summary.init_function = (fun () -> theories_map := Cmap.empty) }
-
-(* declare a new type of object in the environment, "tactic-ring-theory"
-   The functions theory_to_obj and obj_to_theory do the conversions
-   between theories and environement objects. *)
-
-
-let subst_morph subst morph =
-  let plusm' = subst_mps subst morph.plusm in
-  let multm' = subst_mps subst morph.multm in
-  let oppm' = Option.smartmap (subst_mps subst) morph.oppm in
-    if plusm' == morph.plusm
-      && multm' == morph.multm
-      && oppm' == morph.oppm then
-	morph
-    else
-      { plusm = plusm' ;
-	multm = multm' ;
-	oppm = oppm' ;
-      }
-
-let subst_set subst cset =
-  let same = ref true in
-  let copy_subst c newset =
-    let c' = subst_mps subst c in
-      if not (c' == c) then same := false;
-      ConstrSet.add c' newset
-  in
-  let cset' = ConstrSet.fold copy_subst cset ConstrSet.empty in
-    if !same then cset else cset'
-
-let subst_theory subst th =
-  let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in
-  let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in
-  let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in
-  let th_a' = subst_mps subst th.th_a in
-  let th_plus' = subst_mps subst th.th_plus in
-  let th_mult' = subst_mps subst th.th_mult in
-  let th_one' = subst_mps subst th.th_one in
-  let th_zero' = subst_mps subst th.th_zero in
-  let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in
-  let th_eq' = subst_mps subst th.th_eq in
-  let th_t' = subst_mps subst th.th_t in
-  let th_closed' = subst_set subst th.th_closed in
-    if th_equiv' == th.th_equiv
-      && th_setoid_th' == th.th_setoid_th
-      && th_morph' == th.th_morph
-      && th_a' == th.th_a
-      && th_plus' == th.th_plus
-      && th_mult' == th.th_mult
-      && th_one' == th.th_one
-      && th_zero' == th.th_zero
-      && th_opp' == th.th_opp
-      && th_eq' == th.th_eq
-      && th_t' == th.th_t
-      && th_closed' == th.th_closed
-    then
-      th
-    else
-    { th_ring = th.th_ring ;
-      th_abstract = th.th_abstract ;
-      th_setoid = th.th_setoid ;
-      th_equiv = th_equiv' ;
-      th_setoid_th = th_setoid_th' ;
-      th_morph = th_morph' ;
-      th_a = th_a' ;
-      th_plus = th_plus' ;
-      th_mult = th_mult' ;
-      th_one = th_one' ;
-      th_zero = th_zero' ;
-      th_opp = th_opp' ;
-      th_eq = th_eq' ;
-      th_t = th_t' ;
-      th_closed = th_closed' ;
-    }
-
-
-let subst_th (subst,(c,th as obj)) =
-  let c' = subst_mps subst c in
-  let th' = subst_theory subst th in
-    if c' == c && th' == th then obj else
-      (c',th')
-
-
-let theory_to_obj : constr * theory -> obj =
-  let cache_th (_,(c, th)) = theories_map_add (c,th) in
-  declare_object {(default_object "tactic-ring-theory") with
-		    open_function = (fun i o -> if i=1 then cache_th o);
-                    cache_function = cache_th;
-		    subst_function = subst_th;
-		    classify_function = (fun x -> Substitute x) }
-
-(* from the set A, guess the associated theory *)
-(* With this simple solution, the theory to use is automatically guessed *)
-(* But only one theory can be declared for a given Set *)
-
-let guess_theory a =
-  try
-    theories_map_find a
-  with Not_found ->
-    errorlabstrm "Ring"
-      (str "No Declared Ring Theory for " ++
-	 pr_lconstr a ++ fnl () ++
-	 str "Use Add [Semi] Ring to declare it")
-
-(* Looks up an option *)
-
-let unbox = function
-  | Some w -> w
-  | None -> anomaly "Ring : Not in case of a setoid ring."
-
-(* Protects the convertibility test against undue exceptions when using it
-   with untyped terms *)
-
-let safe_pf_conv_x gl c1 c2 = try pf_conv_x gl c1 c2 with _ -> false
-
-
-(* Add a Ring or a Semi-Ring to the database after a type verification *)
-
-let implement_theory env t th args =
-  is_conv env Evd.empty (Typing.type_of env Evd.empty t) (mkLApp (th, args))
-
-(* (\* The following test checks whether the provided morphism is the default *)
-(*    one for the given operation. In principle the test is too strict, since *)
-(*    it should possible to provide another proof for the same fact (proof *)
-(*    irrelevance). In particular, the error message is be not very explicative. *\) *)
-let states_compatibility_for env plus mult opp morphs =
- let check op compat = true in
-(*   is_conv env Evd.empty (Setoid_replace.default_morphism op).Setoid_replace.lem *)
-(*    compat in *)
- check plus morphs.plusm &&
- check mult morphs.multm &&
- (match (opp,morphs.oppm) with
-     None, None -> true
-   | Some opp, Some compat -> check opp compat
-   | _,_ -> assert false)
-
-let add_theory want_ring want_abstract want_setoid a aequiv asetth amorph aplus amult aone azero aopp aeq t cset =
-  if theories_map_mem a then errorlabstrm "Add Semi Ring"
-    (str "A (Semi-)(Setoid-)Ring Structure is already declared for " ++
-       pr_lconstr a);
-  let env = Global.env () in
-    if (want_ring & want_setoid & (
-	not (implement_theory env t coq_Setoid_Ring_Theory
-	  [| a; (unbox aequiv); aplus; amult; aone; azero; (unbox aopp); aeq|])
-        ||
-	not (implement_theory env (unbox asetth) coq_Setoid_Theory
-	  [| a; (unbox aequiv) |]) ||
-        not (states_compatibility_for env aplus amult aopp (unbox amorph))
-        )) then
-      errorlabstrm "addring" (str "Not a valid Setoid-Ring theory");
-    if (not want_ring & want_setoid & (
-        not (implement_theory env t coq_Semi_Setoid_Ring_Theory
-	  [| a; (unbox aequiv); aplus; amult; aone; azero; aeq|]) ||
-	not (implement_theory env (unbox asetth) coq_Setoid_Theory
-	  [| a; (unbox aequiv) |]) ||
-        not (states_compatibility_for env aplus amult aopp (unbox amorph))))
-    then
-      errorlabstrm "addring" (str "Not a valid Semi-Setoid-Ring theory");
-    if (want_ring & not want_setoid &
-	not (implement_theory env t coq_Ring_Theory
-	  [| a; aplus; amult; aone; azero; (unbox aopp); aeq |])) then
-      errorlabstrm "addring" (str "Not a valid Ring theory");
-    if (not want_ring & not want_setoid &
-	not (implement_theory env t coq_Semi_Ring_Theory
-	  [| a; aplus; amult; aone; azero; aeq |])) then
-      errorlabstrm "addring" (str "Not a valid Semi-Ring theory");
-    Lib.add_anonymous_leaf
-      (theory_to_obj
-	 (a, { th_ring = want_ring;
-	       th_abstract = want_abstract;
-	       th_setoid = want_setoid;
-	       th_equiv = aequiv;
-	       th_setoid_th = asetth;
-	       th_morph = amorph;
-	       th_a = a;
-	       th_plus = aplus;
-	       th_mult = amult;
-	       th_one = aone;
-	       th_zero = azero;
-	       th_opp = aopp;
-	       th_eq = aeq;
-	       th_t = t;
-	       th_closed = cset }))
-
-(******** The tactic itself *********)
-
-(*
-   gl : goal sigma
-   th : semi-ring theory (concrete)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-module Constrhash = Hashtbl.Make
-  (struct type t = constr
-	  let equal = eq_constr
-	  let hash = hash_constr
-   end)
-
-let build_spolynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  (* aux creates the spolynom p by a recursive destructuration of c
-     and builds the varmap with side-effects *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_SPplus, [|th.th_a; aux c1; aux c2 |])
-      | App (binop,[|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_SPmult, [|th.th_a; aux c1; aux c2 |])
-      | _ when closed_under th.th_closed c ->
-	  mkLApp(coq_SPconst, [|th.th_a; c |])
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar =
-              mkLApp(coq_SPvar, [|th.th_a; (path_of_int !counter) |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
-  List.map
-    (fun p ->
-       (mkLApp (coq_interp_sp,
-               [|th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
-	mkLApp (coq_interp_cs,
-               [|th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp (coq_spolynomial_simplify,
-			    [| th.th_a; th.th_plus; th.th_mult;
-			       th.th_one; th.th_zero;
-			       th.th_eq; p|])) |]),
-	mkLApp (coq_spolynomial_simplify_ok,
-	        [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
-		  th.th_eq; v; th.th_t; p |])))
-    lp
-
-(*
-   gl : goal sigma
-   th : ring theory (concrete)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-let build_polynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
-      (* The special case of Z.sub *)
-      | App (binop, [|c1; c2|])
-	  when safe_pf_conv_x gl c
-            (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
-	    mkLApp(coq_Pplus,
-                  [|th.th_a; aux c1;
-	            mkLApp(coq_Popp, [|th.th_a; aux c2|]) |])
-      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkLApp(coq_Popp, [|th.th_a; aux c1|])
-      | _ when closed_under th.th_closed c ->
-	  mkLApp(coq_Pconst, [|th.th_a; c |])
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar =
-              mkLApp(coq_Pvar, [|th.th_a; (path_of_int !counter) |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
-  List.map
-    (fun p ->
-       (mkLApp(coq_interp_p,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
-                 (unbox th.th_opp); v; p |])),
-	mkLApp(coq_interp_cs,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp(coq_polynomial_simplify,
-			    [| th.th_a; th.th_plus; th.th_mult;
-			       th.th_one; th.th_zero;
-			       (unbox th.th_opp); th.th_eq; p |])) |]),
-	mkLApp(coq_polynomial_simplify_ok,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
-		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |]))
-    lp
-
-(*
-   gl : goal sigma
-   th : semi-ring theory (abstract)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-let build_aspolynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  (* aux creates the aspolynom p by a recursive destructuration of c
-     and builds the varmap with side-effects *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_ASPplus, [| aux c1; aux c2 |])
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_ASPmult, [| aux c1; aux c2 |])
-      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
-      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = btree_of_array (Array.of_list (List.rev !varlist)) th.th_a in
-  List.map
-    (fun p ->
-       (mkLApp(coq_interp_asp,
-               [| th.th_a; th.th_plus; th.th_mult;
-		  th.th_one; th.th_zero; v; p |]),
-	mkLApp(coq_interp_acs,
-               [| th.th_a; th.th_plus; th.th_mult;
-		  th.th_one; th.th_zero; v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp(coq_aspolynomial_normalize,[|p|])) |]),
-	mkLApp(coq_spolynomial_simplify_ok,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
-		  th.th_eq; v; th.th_t; p |])))
-    lp
-
-(*
-   gl : goal sigma
-   th : ring theory (abstract)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-let build_apolynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_APplus, [| aux c1; aux c2 |])
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_APmult, [| aux c1; aux c2 |])
-      (* The special case of Z.sub *)
-      | App (binop, [|c1; c2|])
-	  when safe_pf_conv_x gl c
-            (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
-	    mkLApp(coq_APplus,
-                   [|aux c1; mkLApp(coq_APopp,[|aux c2|]) |])
-      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkLApp(coq_APopp, [| aux c1 |])
-      | _ when safe_pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
-      | _ when safe_pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar =
-              mkLApp(coq_APvar, [| path_of_int !counter |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
-  List.map
-    (fun p ->
-       (mkLApp(coq_interp_ap,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one;
-		  th.th_zero; (unbox th.th_opp); v; p |]),
-	mkLApp(coq_interp_sacs,
-	       [| th.th_a; th.th_plus; th.th_mult;
-		  th.th_one; th.th_zero; (unbox th.th_opp); v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp(coq_apolynomial_normalize, [|p|])) |]),
-	mkLApp(coq_apolynomial_normalize_ok,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero;
-		  (unbox th.th_opp); th.th_eq; v; th.th_t; p |])))
-    lp
-
-(*
-   gl : goal sigma
-   th : setoid ring theory (concrete)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-let build_setpolynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
-      (* The special case of Z.sub *)
-      | App (binop, [|c1; c2|])
-	  when safe_pf_conv_x gl c
-	    (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->
-	      mkLApp(coq_SetPplus,
-                     [| th.th_a; aux c1;
-			mkLApp(coq_SetPopp, [|th.th_a; aux c2|]) |])
-      | App (unop, [|c1|]) when safe_pf_conv_x gl unop (unbox th.th_opp) ->
-	  mkLApp(coq_SetPopp, [| th.th_a; aux c1 |])
-      | _ when closed_under th.th_closed c ->
-	  mkLApp(coq_SetPconst, [| th.th_a; c |])
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar =
-              mkLApp(coq_SetPvar, [| th.th_a; path_of_int !counter |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
-  List.map
-    (fun p ->
-       (mkLApp(coq_interp_setp,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero;
-                  (unbox th.th_opp); v; p |]),
-	mkLApp(coq_interp_setcs,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp(coq_setpolynomial_simplify,
-			    [| th.th_a; th.th_plus; th.th_mult;
-			       th.th_one; th.th_zero;
-			       (unbox th.th_opp); th.th_eq; p |])) |]),
-	mkLApp(coq_setpolynomial_simplify_ok,
-	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
-                  th.th_mult; th.th_one; th.th_zero;(unbox th.th_opp);
-                  th.th_eq; (unbox th.th_setoid_th);
-		  (unbox th.th_morph).plusm; (unbox th.th_morph).multm;
-		  (unbox (unbox th.th_morph).oppm); v; th.th_t; p |])))
-    lp
-
-(*
-   gl : goal sigma
-   th : semi setoid ring theory (concrete)
-   cl : constr list [c1; c2; ...]
-
-Builds
-   - a list of tuples [(c1, c'1, c''1, c'1_eq_c''1); ... ]
-  where c'i is convertible with ci and
-  c'i_eq_c''i is a proof of equality of c'i and c''i
-
-*)
-
-let build_setspolynom gl th lc =
-  let varhash  = (Constrhash.create 17 : constr Constrhash.t) in
-  let varlist = ref ([] : constr list) in (* list of variables *)
-  let counter = ref 1 in (* number of variables created + 1 *)
-  let rec aux c =
-    match (kind_of_term (strip_outer_cast c)) with
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_plus ->
-	  mkLApp(coq_SetSPplus, [|th.th_a; aux c1; aux c2 |])
-      | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
-	  mkLApp(coq_SetSPmult, [| th.th_a; aux c1; aux c2 |])
-      | _ when closed_under th.th_closed c ->
-	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
-      | _ ->
-	  try Constrhash.find varhash c
-	  with Not_found ->
-	    let newvar =
-              mkLApp(coq_SetSPvar, [|th.th_a; path_of_int !counter |]) in
-	    begin
-	      incr counter;
-	      varlist := c :: !varlist;
-	      Constrhash.add varhash c newvar;
-	      newvar
-	    end
-  in
-  let lp = List.map aux lc in
-  let v = (btree_of_array (Array.of_list (List.rev !varlist)) th.th_a) in
-  List.map
-    (fun p ->
-       (mkLApp(coq_interp_setsp,
-	       [| th.th_a; th.th_plus; th.th_mult; th.th_zero; v; p |]),
-	mkLApp(coq_interp_setcs,
-               [| th.th_a; th.th_plus; th.th_mult; th.th_one; th.th_zero; v;
-		  pf_reduce cbv_betadeltaiota gl
-		    (mkLApp(coq_setspolynomial_simplify,
-			    [| th.th_a; th.th_plus; th.th_mult;
-			       th.th_one; th.th_zero;
-			       th.th_eq; p |])) |]),
-	mkLApp(coq_setspolynomial_simplify_ok,
-	       [| th.th_a; (unbox th.th_equiv); th.th_plus;
-                  th.th_mult; th.th_one; th.th_zero; th.th_eq;
-                  (unbox th.th_setoid_th);
-		  (unbox th.th_morph).plusm;
-                  (unbox th.th_morph).multm; v; th.th_t; p |])))
-    lp
-
-module SectionPathSet =
-  Set.Make(struct
-	     type t = full_path
-	     let compare = Pervasives.compare
-	   end)
-
-(* Avec l'uniformisation des red_kind, on perd ici sur la structure
-   SectionPathSet; peut-être faudra-t-il la déplacer dans Closure *)
-let constants_to_unfold =
-(*  List.fold_right SectionPathSet.add *)
-  let transform s =
-    let sp = path_of_string s in
-    let dir, id = repr_path sp in
-      Globnames.encode_con dir id
-  in
-  List.map transform
-    [ "Coq.ring.Ring_normalize.interp_cs";
-      "Coq.ring.Ring_normalize.interp_var";
-      "Coq.ring.Ring_normalize.interp_vl";
-      "Coq.ring.Ring_abstract.interp_acs";
-      "Coq.ring.Ring_abstract.interp_sacs";
-      "Coq.quote.Quote.varmap_find";
-      (* anciennement des Local devenus Definition *)
-      "Coq.ring.Ring_normalize.ics_aux";
-      "Coq.ring.Ring_normalize.ivl_aux";
-      "Coq.ring.Ring_normalize.interp_m";
-      "Coq.ring.Ring_abstract.iacs_aux";
-      "Coq.ring.Ring_abstract.isacs_aux";
-      "Coq.ring.Setoid_ring_normalize.interp_cs";
-      "Coq.ring.Setoid_ring_normalize.interp_var";
-      "Coq.ring.Setoid_ring_normalize.interp_vl";
-      "Coq.ring.Setoid_ring_normalize.ics_aux";
-      "Coq.ring.Setoid_ring_normalize.ivl_aux";
-      "Coq.ring.Setoid_ring_normalize.interp_m";
-    ]
-(*    SectionPathSet.empty *)
-
-(* Unfolds the functions interp and find_btree in the term c of goal gl *)
-open RedFlags
-let polynom_unfold_tac =
-  let flags =
-    (mkflags(fBETA::fIOTA::(List.map fCONST constants_to_unfold))) in
-  reduct_in_concl (cbv_norm_flags flags,DEFAULTcast)
-
-let polynom_unfold_tac_in_term gl =
-  let flags =
-    (mkflags(fBETA::fIOTA::fZETA::(List.map fCONST constants_to_unfold)))
-  in
-  cbv_norm_flags flags (pf_env gl) (project gl)
-
-(* lc : constr list *)
-(* th : theory associated to t *)
-(* op : clause (None for conclusion or Some id for hypothesis id) *)
-(* gl : goal  *)
-(* Does the rewriting c_i -> (interp R RC v (polynomial_simplify p_i))
-   where the ring R, the Ring theory RC, the varmap v and the polynomials p_i
-   are guessed and such that c_i = (interp R RC v p_i) *)
-let raw_polynom th op lc gl =
-  (* first we sort the terms : if t' is a subterm of t it must appear
-     after t in the list. This is to avoid that the normalization of t'
-     modifies t in a non-desired way *)
-  let lc = sort_subterm gl lc in
-  let ltriplets =
-    if th.th_setoid then
-      if th.th_ring
-      then build_setpolynom gl th lc
-      else build_setspolynom gl th lc
-    else
-      if th.th_ring then
-	if th.th_abstract
-	then build_apolynom gl th lc
-	else build_polynom gl th lc
-      else
-	if th.th_abstract
-	then build_aspolynom gl th lc
-	else build_spolynom gl th lc in
-  let polynom_tac =
-    List.fold_right2
-      (fun ci (c'i, c''i, c'i_eq_c''i) tac ->
-         let c'''i =
-	   if !term_quality then polynom_unfold_tac_in_term gl c''i else c''i
-	 in
-         if !term_quality && safe_pf_conv_x gl c'''i ci then
-	   tac (* convertible terms *)
-         else if th.th_setoid
-	 then
-           (tclORELSE
-              (tclORELSE
-		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkLApp(coq_seq_sym,
-				  [| th.th_a; (unbox th.th_equiv);
-                                     (unbox th.th_setoid_th);
-				     c'''i; ci; c'i_eq_c''i |]))))
-	      (tclTHENS
-		 (tclORELSE
-                   (Equality.general_rewrite true
-		     Locus.AllOccurrences true false c'i_eq_c''i)
-                   (Equality.general_rewrite false
-		     Locus.AllOccurrences true false c'i_eq_c''i))
-                 [tac]))
-	 else
-           (tclORELSE
-              (tclORELSE
-		 (h_exact c'i_eq_c''i)
-		 (h_exact (mkApp(build_coq_eq_sym (),
-				 [|th.th_a; c'''i; ci; c'i_eq_c''i |]))))
-	      (tclTHENS
-		 (elim_type
-		    (mkApp(build_coq_eq (), [|th.th_a; c'''i; ci |])))
-		 [ tac;
-                   h_exact c'i_eq_c''i ]))
-)
-      lc ltriplets polynom_unfold_tac
-  in
-  polynom_tac gl
-
-let guess_eq_tac th =
-  (tclORELSE reflexivity
-     (tclTHEN
-	polynom_unfold_tac
-        (tclTHEN
-	   (* Normalized sums associate on the right *)
-	   (tclREPEAT
-	      (tclTHENFIRST
-		 (apply (mkApp(build_coq_f_equal2 (),
-		               [| th.th_a; th.th_a; th.th_a;
-				  th.th_plus |])))
-		 reflexivity))
-	   (tclTRY
-	      (tclTHENLAST
-		 (apply (mkApp(build_coq_f_equal2 (),
-			       [| th.th_a; th.th_a; th.th_a;
-				  th.th_plus |])))
-		 reflexivity)))))
-
-let guess_equiv_tac th =
-  (tclORELSE (apply (mkLApp(coq_seq_refl,
-			    [| th.th_a; (unbox th.th_equiv);
-			       (unbox th.th_setoid_th)|])))
-     (tclTHEN
-	polynom_unfold_tac
-	(tclREPEAT
-	   (tclORELSE
-	      (apply (unbox th.th_morph).plusm)
-	      (apply (unbox th.th_morph).multm)))))
-
-let match_with_equiv c = match (kind_of_term c) with
-  | App (e,a) ->
-      if (List.mem e []) (*  (Setoid_replace.equiv_list ())) *)
-      then Some (decompose_app c)
-      else None
-  | _ -> None
-
-let polynom lc gl =
-  Coqlib.check_required_library ["Coq";"ring";"LegacyRing"];
-  match lc with
-   (* If no argument is given, try to recognize either an equality or
-      a declared relation with arguments c1 ... cn,
-      do "Ring c1 c2 ... cn" and then try to apply the simplification
-      theorems declared for the relation *)
-    | [] ->
-	(try
-	  match Hipattern.match_with_equation (pf_concl gl) with
-	   | _,_,Hipattern.PolymorphicLeibnizEq (t,c1,c2) ->
-	       let th = guess_theory t in
-	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
-	   | _,_,Hipattern.HeterogenousEq (t1,c1,t2,c2)
-	       when safe_pf_conv_x gl t1 t2 ->
-	       let th = guess_theory t1 in
-	       (tclTHEN (raw_polynom th None [c1;c2]) (guess_eq_tac th)) gl
-	   | _ -> raise Exit
-	  with Hipattern.NoEquationFound | Exit ->
-	          (match match_with_equiv (pf_concl gl) with
-		     | Some (equiv, c1::args) ->
-			 let t = (pf_type_of gl c1) in
-			 let th = (guess_theory t) in
-			   if List.exists
-			     (fun c2 -> not (safe_pf_conv_x gl t (pf_type_of gl c2))) args
-			   then
-			     errorlabstrm "Ring :"
-			       (str" All terms must have the same type");
-			   (tclTHEN (raw_polynom th None (c1::args)) (guess_equiv_tac th)) gl
-		     | _ -> errorlabstrm "polynom :"
-			 (str" This goal is not an equality nor a setoid equivalence")))
-    (* Elsewhere, guess the theory, check that all terms have the same type
-       and apply raw_polynom *)
-    | c :: lc' ->
-	let t = pf_type_of gl c in
-	let th = guess_theory t in
-	  if List.exists
-	    (fun c1 -> not (safe_pf_conv_x gl t (pf_type_of gl c1))) lc'
-	  then
-	    errorlabstrm "Ring :"
-	      (str" All terms must have the same type");
-	  (tclTHEN (raw_polynom th None lc) polynom_unfold_tac) gl
diff --git a/plugins/ring/ring_plugin.mllib b/plugins/ring/ring_plugin.mllib
deleted file mode 100644
index 3c5f995f7..000000000
--- a/plugins/ring/ring_plugin.mllib
+++ /dev/null
@@ -1,3 +0,0 @@
-Ring
-G_ring
-Ring_plugin_mod
diff --git a/plugins/ring/vo.itarget b/plugins/ring/vo.itarget
deleted file mode 100644
index da387be8c..000000000
--- a/plugins/ring/vo.itarget
+++ /dev/null
@@ -1,10 +0,0 @@
-LegacyArithRing.vo
-LegacyNArithRing.vo
-LegacyRing_theory.vo
-LegacyRing.vo
-LegacyZArithRing.vo
-Ring_abstract.vo
-Ring_normalize.vo
-Setoid_ring_normalize.vo
-Setoid_ring_theory.vo
-Setoid_ring.vo
diff --git a/plugins/setoid_ring/Ring_equiv.v b/plugins/setoid_ring/Ring_equiv.v
deleted file mode 100644
index 945f6c684..000000000
--- a/plugins/setoid_ring/Ring_equiv.v
+++ /dev/null
@@ -1,74 +0,0 @@
-Require Import Setoid_ring_theory.
-Require Import LegacyRing_theory.
-Require Import Ring_theory.
-
-Set Implicit Arguments.
-
-Section Old2New.
-
-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.
-Variable R : Ring_Theory Aplus Amult Aone Azero Aopp Aeq.
-
-Let Aminus := fun x y => Aplus x (Aopp y).
-
-Lemma ring_equiv1 :
-  ring_theory Azero Aone Aplus Amult Aminus Aopp (eq (A:=A)).
-Proof.
-destruct R.
-split;  eauto.
-Qed.
-
-End Old2New.
-
-Section New2OldRing.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable Rth : ring_theory rO rI radd rmul rsub ropp (eq (A:=R)).
-
- Variable reqb : R -> R -> bool.
- Variable reqb_ok : forall x y, reqb x y = true -> x = y.
-
- Lemma ring_equiv2 :
-   Ring_Theory radd  rmul rI rO ropp reqb.
-Proof.
-elim Rth; intros; constructor;  eauto.
-intros.
-apply reqb_ok.
-destruct (reqb x y); trivial; intros.
-elim H.
-Qed.
-
- Definition default_eqb : R -> R -> bool := fun x y => false.
- Lemma default_eqb_ok : forall x y, default_eqb x y = true -> x = y.
-Proof.
-discriminate 1.
-Qed.
-
-End New2OldRing.
-
-Section New2OldSemiRing.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul: R->R->R).
- Variable SRth : semi_ring_theory rO rI radd rmul (eq (A:=R)).
-
- Variable reqb : R -> R -> bool.
- Variable reqb_ok : forall x y, reqb x y = true -> x = y.
-
- Lemma sring_equiv2 :
-   Semi_Ring_Theory radd rmul rI rO reqb.
-Proof.
-elim SRth; intros; constructor;  eauto.
-intros.
-apply reqb_ok.
-destruct (reqb x y); trivial; intros.
-elim H.
-Qed.
-
-End New2OldSemiRing.
diff --git a/plugins/setoid_ring/vo.itarget b/plugins/setoid_ring/vo.itarget
index 580df9b55..595ba55ec 100644
--- a/plugins/setoid_ring/vo.itarget
+++ b/plugins/setoid_ring/vo.itarget
@@ -7,7 +7,6 @@ InitialRing.vo
 NArithRing.vo
 RealField.vo
 Ring_base.vo
-Ring_equiv.vo
 Ring_polynom.vo
 Ring_tac.vo
 Ring_theory.vo
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
deleted file mode 100644
index df4da431f..000000000
--- a/test-suite/success/LegacyField.v
+++ /dev/null
@@ -1,76 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(**** Tests of Field with real numbers ****)
-
-Require Import Reals LegacyRfield.
-
-(* Example 1 *)
-Goal
-forall eps : R,
-(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 2 *)
-Goal
-forall (f g : R -> R) (x0 x1 : R),
-((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R =
-((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 3 *)
-Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 4 *)
-Goal
-forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 5 *)
-Goal forall a : R, 1%R = (1 * (1 / a) * a)%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 6 *)
-Goal forall a b : R, b = (b * / a * a)%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 7 *)
-Goal forall a b : R, b = (b * (1 / a) * a)%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
-
-(* Example 8 *)
-Goal
-forall x y : R,
-(x * (1 / x + x / (x + y)))%R =
-(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R.
-Proof.
-  intros.
-   legacy field.
-Abort.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index 3730bcd7f..2400055aa 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -187,25 +187,3 @@ rewrite Q2R_inv; auto.
 Qed.
 
 Hint Rewrite Q2R_plus Q2R_mult Q2R_opp Q2R_minus Q2R_inv Q2R_div : q2r_simpl.
-
-Section LegacyQField.
-
-(** In the past, the field tactic was not able to deal with setoid datatypes,
-    so translating from Q to R and applying field on reals was a workaround.
-    See now Qfield for a direct field tactic on Q. *)
-
-Ltac QField := apply eqR_Qeq; autorewrite with q2r_simpl; try field; auto.
-
-(** Examples of use: *)
-
-Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z).
-intros; QField.
-Qed.
-
-Let ex2 : forall x y : Q, ~ y==0 -> (x/y)*y == x.
-intros; QField.
-intro; apply H; apply eqR_Qeq.
-rewrite H0; unfold Q2R; simpl; field; auto with real.
-Qed.
-
-End LegacyQField.
diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v
deleted file mode 100644
index 8a62eb866..000000000
--- a/theories/Reals/LegacyRfield.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export Raxioms.
-Require Export LegacyField.
-Import LegacyRing_theory.
-
-Section LegacyRfield.
-
-Open Scope R_scope.
-
-Lemma RLegacyTheory : Ring_Theory Rplus Rmult 1 0 Ropp (fun x y:R => false).
-  split.
-  exact Rplus_comm.
-  symmetry ; apply Rplus_assoc.
-  exact Rmult_comm.
-  symmetry ; apply Rmult_assoc.
-  intro; apply Rplus_0_l.
-  intro; apply Rmult_1_l.
-  exact Rplus_opp_r.
-  intros.
-  rewrite Rmult_comm.
-  rewrite (Rmult_comm n p).
-  rewrite (Rmult_comm m p).
-  apply Rmult_plus_distr_l.
-  intros; contradiction.
-Defined.
-
-End LegacyRfield.
-
-Add Legacy Field
-R Rplus Rmult 1%R 0%R Ropp (fun x y:R => false) Rinv RLegacyTheory Rinv_l
-  with minus := Rminus div := Rdiv.
diff --git a/theories/Reals/vo.itarget b/theories/Reals/vo.itarget
index 36dd0f56d..0c8f0b976 100644
--- a/theories/Reals/vo.itarget
+++ b/theories/Reals/vo.itarget
@@ -8,7 +8,6 @@ Cos_rel.vo
 DiscrR.vo
 Exp_prop.vo
 Integration.vo
-LegacyRfield.vo
 Machin.vo
 MVT.vo
 NewtonInt.vo