Merge branch 'experimental/upstream' into upstream

12 files changed, 270 insertions, 299 deletions

diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 2de16bc1..089dec02 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Instantiation of the Ring tactic for the naturals of Arith $*)
 
 Require Import Bool.
@@ -15,9 +13,9 @@ Require Export LegacyRing.
 Require Export Arith.
 Require Import Eqdep_dec.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
-Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
+Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
   | O, O => true
   | S n', S m' => nateq n' m'
@@ -77,14 +75,14 @@ Ltac rewrite_S_to_plus :=
        (**)  (**)
        rewrite_S_to_plus_term X1
        with t2 := rewrite_S_to_plus_term X2 in
-       change (t1 = t2) 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) 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
index ae7e62e0..7f1597a1 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyNArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Instantiation of the Ring tactic for the binary natural numbers *)
 
 Require Import Bool.
@@ -16,7 +14,7 @@ Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
 
-Unboxed Definition Neq (n m:N) :=
+Definition Neq (n m:N) :=
   match (n ?= m)%N with
   | Datatypes.Eq => true
   | _ => false
@@ -24,23 +22,22 @@ Unboxed Definition Neq (n m:N) :=
 
 Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
   intros n m H; unfold Neq in H.
-  apply Ncompare_Eq_eq.
+  apply N.compare_eq.
   destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
 Qed.
 
-Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
+Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
   split.
-    apply Nplus_comm.
-    apply Nplus_assoc.
-    apply Nmult_comm.
-    apply Nmult_assoc.
-    apply Nplus_0_l.
-    apply Nmult_1_l.
-    apply Nmult_0_l.
-    apply Nmult_plus_distr_r.
-(*    apply Nplus_reg_l.*)
+    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 Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+  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
index e53e60d3..d4f40081 100644
--- a/plugins/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Bool.
 Require Export LegacyRing_theory.
 Require Export Quote.
@@ -21,7 +19,7 @@ Declare ML Module "ring_plugin".
 
 Definition BoolTheory :
   Ring_Theory xorb andb true false (fun b:bool => b) eqb.
-split; simpl in |- *.
+split; simpl.
 destruct n; destruct m; reflexivity.
 destruct n; destruct m; destruct p; reflexivity.
 destruct n; destruct m; reflexivity.
@@ -30,7 +28,7 @@ destruct n; reflexivity.
 destruct n; reflexivity.
 destruct n; reflexivity.
 destruct n; destruct m; destruct p; reflexivity.
-destruct x; destruct y; reflexivity || simpl in |- *; tauto.
+destruct x; destruct y; reflexivity || simpl; tauto.
 Defined.
 
 Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v
index bf61aee1..09de1bb4 100644
--- a/plugins/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyRing_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Bool.
 
 Set Implicit Arguments.
@@ -60,22 +58,22 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_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  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
 intros.
@@ -102,7 +100,7 @@ eauto.
 Qed.
 
 Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry  in |- *; apply SR_distr_right. Qed.
+symmetry ; apply SR_distr_right. Qed.
 
 Lemma SR_mult_zero_right : forall n:A, n * 0 = 0.
 intro; rewrite mult_comm; eauto.
@@ -178,22 +176,22 @@ Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_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  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_opp_def2 : forall n:A, 0 = n + - n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
 intros.
@@ -216,7 +214,7 @@ 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 in |- *.
+pattern a at 1.
 rewrite <- H.
 rewrite <- plus_assoc.
 rewrite opp_def.
@@ -235,7 +233,7 @@ Qed.
 Hint Resolve Th_mult_zero_left.
 
 Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z.
 intros.
@@ -257,7 +255,7 @@ Qed.
 Hint Resolve Th_opp_mult_left.
 
 Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y).
-symmetry  in |- *; eauto. Qed.
+symmetry ; eauto. Qed.
 
 Lemma Th_mult_zero_right : forall n:A, n * 0 = 0.
 intro; elim mult_comm; eauto.
@@ -308,14 +306,14 @@ Qed.
 Hint Resolve Th_opp_opp.
 
 Lemma Th_opp_opp2 : forall n:A, n = - - n.
-symmetry  in |- *; eauto. Qed.
+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  in |- *; apply Th_mult_opp_opp. Qed.
+symmetry ; apply Th_mult_opp_opp. Qed.
 
 Lemma Th_opp_zero : - 0 = 0.
 rewrite <- (plus_zero_left (- 0)).
@@ -344,7 +342,7 @@ eauto.
 Qed.
 
 Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry  in |- *; apply Th_distr_right.
+symmetry ; apply Th_distr_right.
 Qed.
 
 End Theory_of_rings.
@@ -359,7 +357,7 @@ Definition Semi_Ring_Theory_of :
     Ring_Theory Aplus Amult Aone Azero Aopp Aeq ->
     Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
 intros until 1; case H.
-split; intros; simpl in |- *; eauto.
+split; intros; simpl; eauto.
 Defined.
 
 (* Every ring can be viewed as a semi-ring : this property will be used
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index d1412104..3f01a5c3 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: LegacyZArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* Instantiation of the Ring tactic for the binary integers of ZArith *)
 
 Require Export LegacyArithRing.
@@ -15,7 +13,7 @@ Require Export ZArith_base.
 Require Import Eqdep_dec.
 Require Import LegacyRing.
 
-Unboxed Definition Zeq (x y:Z) :=
+Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
   | Datatypes.Eq => true
   | _ => false
@@ -23,15 +21,15 @@ Unboxed Definition Zeq (x y:Z) :=
 
 Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
   intros x y H; unfold Zeq in H.
-  apply Zcompare_Eq_eq.
+  apply Z.compare_eq.
   destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ].
 Qed.
 
-Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
+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 Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+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
index e6e2dda9..a00b7bcd 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -1,19 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring_abstract.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Import LegacyRing_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
-Unset Boxed Definitions.
-
 Section abstract_semi_rings.
 
 Inductive aspolynomial : Type :=
@@ -141,14 +137,13 @@ 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 refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+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 in |- *; intros.
+  simple induction s; simpl; intros.
   trivial.
   reflexivity.
 Qed.
@@ -163,8 +158,8 @@ Lemma abstract_varlist_insert_ok :
   simple induction s.
   trivial.
 
-  simpl in |- *; intros.
-  elim (varlist_lt l v); simpl in |- *.
+  simpl; intros.
+  elim (varlist_lt l v); simpl.
   eauto.
   rewrite iacs_aux_ok.
   rewrite H; auto.
@@ -182,13 +177,13 @@ Proof.
 
   auto.
 
-  simpl in |- *; elim (varlist_lt v v0); simpl in |- *.
+  simpl; elim (varlist_lt v v0); simpl.
   repeat rewrite iacs_aux_ok.
-  rewrite H; simpl in |- *; auto.
+  rewrite H; simpl; auto.
 
   simpl in H0.
   repeat rewrite iacs_aux_ok.
-  rewrite H0. simpl in |- *; auto.
+  rewrite H0. simpl; auto.
 Qed.
 
 Lemma abstract_sum_scalar_ok :
@@ -197,9 +192,9 @@ Lemma abstract_sum_scalar_ok :
    Amult (interp_vl Amult Aone Azero vm l) (interp_acs s).
 Proof.
   simple induction s.
-  simpl in |- *; eauto.
+  simpl; eauto.
 
-  simpl in |- *; intros.
+  simpl; intros.
   rewrite iacs_aux_ok.
   rewrite abstract_varlist_insert_ok.
   rewrite H.
@@ -213,22 +208,22 @@ Lemma abstract_sum_prod_ok :
 
 Proof.
   simple induction x.
-  intros; simpl in |- *; eauto.
+  intros; simpl; eauto.
 
   destruct y as [| v0 a0]; intros.
 
-  simpl in |- *; rewrite H; eauto.
+  simpl; rewrite H; eauto.
 
-  unfold abstract_sum_prod in |- *; fold abstract_sum_prod in |- *.
+  unfold abstract_sum_prod; fold abstract_sum_prod.
   rewrite abstract_sum_merge_ok.
   rewrite abstract_sum_scalar_ok.
-  rewrite H; simpl in |- *; auto.
+  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 in |- *; intros; trivial.
+  simple induction x; simpl; intros; trivial.
   rewrite abstract_sum_merge_ok.
   rewrite H; rewrite H0; eauto.
   rewrite abstract_sum_prod_ok.
@@ -450,14 +445,13 @@ 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 refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+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 in |- *; intros.
+  simple induction s; simpl; intros.
   trivial.
   reflexivity.
   reflexivity.
@@ -466,15 +460,15 @@ Qed.
 Hint Extern 10 (_ = _ :>A) => rewrite isacs_aux_ok: core.
 
 Ltac solve1 v v0 H H0 :=
-  simpl in |- *; elim (varlist_lt v v0); simpl in |- *; rewrite isacs_aux_ok;
-   [ rewrite H; simpl in |- *; auto | simpl in H0; rewrite H0; auto ].
+  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 in |- *; auto.
+  intro; simpl; auto.
 
   simple induction y; intros.
 
@@ -482,8 +476,8 @@ Lemma signed_sum_merge_ok :
 
   solve1 v v0 H H0.
 
-  simpl in |- *; generalize (varlist_eq_prop v v0).
-  elim (varlist_eq v v0); simpl in |- *.
+  simpl; generalize (varlist_eq_prop v v0).
+  elim (varlist_eq v v0); simpl.
 
   intro Heq; rewrite (Heq I).
   rewrite H.
@@ -503,8 +497,8 @@ Lemma signed_sum_merge_ok :
 
   auto.
 
-  simpl in |- *; generalize (varlist_eq_prop v v0).
-  elim (varlist_eq v v0); simpl in |- *.
+  simpl; generalize (varlist_eq_prop v v0).
+  elim (varlist_eq v v0); simpl.
 
   intro Heq; rewrite (Heq I).
   rewrite H.
@@ -522,7 +516,7 @@ Lemma signed_sum_merge_ok :
 Qed.
 
 Ltac solve2 l v H :=
-  elim (varlist_lt l v); simpl in |- *; rewrite isacs_aux_ok;
+  elim (varlist_lt l v); simpl; rewrite isacs_aux_ok;
    [ auto | rewrite H; auto ].
 
 Lemma plus_varlist_insert_ok :
@@ -534,12 +528,12 @@ Proof.
   simple induction s.
   trivial.
 
-  simpl in |- *; intros.
+  simpl; intros.
   solve2 l v H.
 
-  simpl in |- *; intros.
+  simpl; intros.
   generalize (varlist_eq_prop l v).
-  elim (varlist_eq l v); simpl in |- *.
+  elim (varlist_eq l v); simpl.
 
   intro Heq; rewrite (Heq I).
   repeat rewrite isacs_aux_ok.
@@ -561,9 +555,9 @@ Proof.
   simple induction s.
   trivial.
 
-  simpl in |- *; intros.
+  simpl; intros.
   generalize (varlist_eq_prop l v).
-  elim (varlist_eq l v); simpl in |- *.
+  elim (varlist_eq l v); simpl.
 
   intro Heq; rewrite (Heq I).
   repeat rewrite isacs_aux_ok.
@@ -574,10 +568,10 @@ Proof.
   rewrite (Th_opp_def T).
   auto.
 
-  simpl in |- *; intros.
+  simpl; intros.
   solve2 l v H.
 
-  simpl in |- *; intros; solve2 l v H.
+  simpl; intros; solve2 l v H.
 
 Qed.
 
@@ -585,9 +579,9 @@ Lemma signed_sum_opp_ok :
  forall s:signed_sum, interp_sacs (signed_sum_opp s) = Aopp (interp_sacs s).
 Proof.
 
-  simple induction s; simpl in |- *; intros.
+  simple induction s; simpl; intros.
 
-  symmetry  in |- *; apply (Th_opp_zero T).
+  symmetry ; apply (Th_opp_zero T).
 
   repeat rewrite isacs_aux_ok.
   rewrite H.
@@ -611,14 +605,14 @@ Proof.
   simple induction s.
   trivial.
 
-  simpl in |- *; intros.
+  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 in |- *; intros.
+  simpl; intros.
   rewrite minus_varlist_insert_ok.
   repeat rewrite isacs_aux_ok.
   rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
@@ -635,11 +629,11 @@ Lemma minus_sum_scalar_ok :
    Aopp (Amult (interp_vl Amult Aone Azero vm l) (interp_sacs s)).
 Proof.
 
-  simple induction s; simpl in |- *; intros.
+  simple induction s; simpl; intros.
 
-  rewrite (Th_mult_zero_right T); symmetry  in |- *; apply (Th_opp_zero T).
+  rewrite (Th_mult_zero_right T); symmetry ; apply (Th_opp_zero T).
 
-  simpl in |- *; intros.
+  simpl; intros.
   rewrite minus_varlist_insert_ok.
   rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
   repeat rewrite isacs_aux_ok.
@@ -648,7 +642,7 @@ Proof.
   rewrite (Th_plus_opp_opp T).
   reflexivity.
 
-  simpl in |- *; intros.
+  simpl; intros.
   rewrite plus_varlist_insert_ok.
   repeat rewrite isacs_aux_ok.
   rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
@@ -668,16 +662,16 @@ Proof.
 
   simple induction x.
 
-  simpl in |- *; eauto 1.
+  simpl; eauto 1.
 
-  intros; simpl in |- *.
+  intros; simpl.
   rewrite signed_sum_merge_ok.
   rewrite plus_sum_scalar_ok.
   repeat rewrite isacs_aux_ok.
   rewrite H.
   auto.
 
-  intros; simpl in |- *.
+  intros; simpl.
   repeat rewrite isacs_aux_ok.
   rewrite signed_sum_merge_ok.
   rewrite minus_sum_scalar_ok.
@@ -691,7 +685,7 @@ Qed.
 Theorem apolynomial_normalize_ok :
  forall p:apolynomial, interp_sacs (apolynomial_normalize p) = interp_ap p.
 Proof.
-  simple induction p; simpl in |- *; auto 1.
+  simple induction p; simpl; auto 1.
   intros.
     rewrite signed_sum_merge_ok.
     rewrite H; rewrite H0; reflexivity.
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index dd4e7314..d286208a 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -1,25 +1,22 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Import LegacyRing_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 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 in |- *; trivial; intros.
+  case (index_eq n m); simpl; trivial; intros.
   contradiction.
 Qed.
 
@@ -368,14 +365,13 @@ 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 refl_equal sym_equal trans_equal.
-(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
+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 in |- *; intros.
+  simpl; intros.
   generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
   rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
 Qed.
@@ -384,7 +380,7 @@ 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 in |- *; intros.
+  simple induction v; simpl; intros.
   trivial.
   rewrite H; trivial.
 Qed.
@@ -394,14 +390,14 @@ Lemma varlist_merge_ok :
    interp_vl (varlist_merge x y) = Amult (interp_vl x) (interp_vl y).
 Proof.
   simple induction x.
-  simpl in |- *; trivial.
+  simpl; trivial.
   simple induction y.
-  simpl in |- *; trivial.
-  simpl in |- *; intros.
-  elim (index_lt i i0); simpl in |- *; intros.
+  simpl; trivial.
+  simpl; intros.
+  elim (index_lt i i0); simpl; intros.
 
   repeat rewrite ivl_aux_ok.
-  rewrite H. simpl in |- *.
+  rewrite H. simpl.
   rewrite ivl_aux_ok.
   eauto.
 
@@ -414,7 +410,7 @@ 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 in |- *; intros.
+  simple induction s; simpl; intros.
   trivial.
   reflexivity.
   reflexivity.
@@ -424,7 +420,7 @@ 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 in |- *; trivial.
+  simpl; trivial.
   reflexivity.
 Qed.
 
@@ -432,10 +428,10 @@ 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 in |- *.
+simple induction x; simpl.
 trivial.
 
-simple induction y; simpl in |- *; intros.
+simple induction y; simpl; intros.
 (* monom and nil *)
 eauto.
 
@@ -443,25 +439,25 @@ eauto.
 generalize (varlist_eq_prop v v0).
 elim (varlist_eq v v0).
 intros; rewrite (H1 I).
-simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
+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 in |- *.
+elim (varlist_lt v v0); simpl.
 repeat rewrite ics_aux_ok.
-rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
+rewrite H; simpl; rewrite ics_aux_ok; eauto.
 
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
+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 in |- *; repeat rewrite ics_aux_ok; rewrite H.
+simpl; repeat rewrite ics_aux_ok; rewrite H.
 repeat rewrite interp_m_ok.
 rewrite (SR_distr_left T).
 repeat rewrite <- (SR_plus_assoc T).
@@ -469,13 +465,13 @@ apply f_equal with (f := Aplus (Amult a (interp_vl v0))).
 rewrite (SR_mult_one_left T).
 trivial.
 
-elim (varlist_lt v v0); simpl in |- *.
+elim (varlist_lt v v0); simpl.
 repeat rewrite ics_aux_ok.
-rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
+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 in |- *; intros.
+simple induction y; simpl; intros.
 (* varlist and nil *)
 trivial.
 
@@ -483,7 +479,7 @@ trivial.
 generalize (varlist_eq_prop v v0).
 elim (varlist_eq v v0).
 intros; rewrite (H1 I).
-simpl in |- *; repeat rewrite ics_aux_ok; rewrite H.
+simpl; repeat rewrite ics_aux_ok; rewrite H.
 repeat rewrite interp_m_ok.
 rewrite (SR_distr_left T).
 repeat rewrite <- (SR_plus_assoc T).
@@ -491,17 +487,17 @@ rewrite (SR_mult_one_left T).
 apply f_equal with (f := Aplus (interp_vl v0)).
 trivial.
 
-elim (varlist_lt v v0); simpl in |- *.
+elim (varlist_lt v v0); simpl.
 repeat rewrite ics_aux_ok.
-rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
+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 in |- *; repeat rewrite ics_aux_ok; rewrite H.
+simpl; repeat rewrite ics_aux_ok; rewrite H.
 repeat rewrite interp_m_ok.
 rewrite (SR_distr_left T).
 repeat rewrite <- (SR_plus_assoc T).
@@ -509,10 +505,10 @@ rewrite (SR_mult_one_left T).
 apply f_equal with (f := Aplus (interp_vl v0)).
 trivial.
 
-elim (varlist_lt v v0); simpl in |- *.
+elim (varlist_lt v v0); simpl.
 repeat rewrite ics_aux_ok.
-rewrite H; simpl in |- *; rewrite ics_aux_ok; eauto.
-rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl in |- *;
+rewrite H; simpl; rewrite ics_aux_ok; eauto.
+rewrite ics_aux_ok; rewrite H0; repeat rewrite ics_aux_ok; simpl;
  eauto.
 Qed.
 
@@ -522,24 +518,24 @@ Lemma monom_insert_ok :
    Aplus (Amult a (interp_vl l)) (interp_cs s).
 intros; generalize s; simple induction s0.
 
-simpl in |- *; rewrite interp_m_ok; trivial.
+simpl; rewrite interp_m_ok; trivial.
 
-simpl in |- *; intros.
+simpl; intros.
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
+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 in |- *;
+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 in |- *; intros.
+simpl; intros.
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
+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 in |- *;
+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 ].
@@ -550,24 +546,24 @@ Lemma varlist_insert_ok :
    interp_cs (varlist_insert l s) = Aplus (interp_vl l) (interp_cs s).
 intros; generalize s; simple induction s0.
 
-simpl in |- *; trivial.
+simpl; trivial.
 
-simpl in |- *; intros.
+simpl; intros.
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
+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 in |- *;
+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 in |- *; intros.
+simpl; intros.
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *; rewrite interp_m_ok;
+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 in |- *;
+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 ].
@@ -577,9 +573,9 @@ 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 in |- *; eauto.
+simpl; eauto.
 
-simpl in |- *; intros.
+simpl; intros.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
 rewrite H.
@@ -587,7 +583,7 @@ rewrite (SR_distr_right T).
 repeat rewrite <- (SR_mult_assoc T).
 reflexivity.
 
-simpl in |- *; intros.
+simpl; intros.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
 rewrite H.
@@ -600,9 +596,9 @@ 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 in |- *; trivial.
+simpl; trivial.
 
-simpl in |- *; intros.
+simpl; intros.
 rewrite monom_insert_ok.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
@@ -614,7 +610,7 @@ repeat rewrite <- (SR_plus_assoc T).
 rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
 reflexivity.
 
-simpl in |- *; intros.
+simpl; intros.
 rewrite varlist_insert_ok.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
@@ -631,9 +627,9 @@ Lemma canonical_sum_scalar3_ok :
    interp_cs (canonical_sum_scalar3 c l s) =
    Amult c (Amult (interp_vl l) (interp_cs s)).
 simple induction s.
-simpl in |- *; repeat rewrite (SR_mult_zero_right T); reflexivity.
+simpl; repeat rewrite (SR_mult_zero_right T); reflexivity.
 
-simpl in |- *; intros.
+simpl; intros.
 rewrite monom_insert_ok.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
@@ -645,7 +641,7 @@ repeat rewrite <- (SR_plus_assoc T).
 rewrite (SR_mult_permute T a (interp_vl l) (interp_vl v)).
 reflexivity.
 
-simpl in |- *; intros.
+simpl; intros.
 rewrite monom_insert_ok.
 repeat rewrite ics_aux_ok.
 repeat rewrite interp_m_ok.
@@ -661,7 +657,7 @@ 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 in |- *; intros.
+simple induction x; simpl; intros.
 trivial.
 
 rewrite canonical_sum_merge_ok.
@@ -670,7 +666,7 @@ rewrite ics_aux_ok.
 rewrite interp_m_ok.
 rewrite H.
 rewrite (SR_mult_assoc T a (interp_vl v) (interp_cs y)).
-symmetry  in |- *.
+symmetry .
 eauto.
 
 rewrite canonical_sum_merge_ok.
@@ -682,7 +678,7 @@ Qed.
 
 Theorem spolynomial_normalize_ok :
  forall p:spolynomial, interp_cs (spolynomial_normalize p) = interp_sp p.
-simple induction p; simpl in |- *; intros.
+simple induction p; simpl; intros.
 
 reflexivity.
 reflexivity.
@@ -703,7 +699,7 @@ simple induction s.
 reflexivity.
 
 (* cons_monom *)
-simpl in |- *; intros.
+simpl; intros.
 generalize (SR_eq_prop T a Azero).
 elim (Aeq a Azero).
 intro Heq; rewrite (Heq I).
@@ -713,25 +709,25 @@ rewrite interp_m_ok.
 rewrite (SR_mult_zero_left T).
 trivial.
 
-intros; simpl in |- *.
+intros; simpl.
 generalize (SR_eq_prop T a Aone).
 elim (Aeq a Aone).
 intro Heq; rewrite (Heq I).
-simpl in |- *.
+simpl.
 repeat rewrite ics_aux_ok.
 rewrite interp_m_ok.
 rewrite H.
 rewrite (SR_mult_one_left T).
 reflexivity.
 
-simpl in |- *.
+simpl.
 repeat rewrite ics_aux_ok.
 rewrite interp_m_ok.
 rewrite H.
 reflexivity.
 
 (* cons_varlist *)
-simpl in |- *; intros.
+simpl; intros.
 repeat rewrite ics_aux_ok.
 rewrite H.
 reflexivity.
@@ -741,7 +737,7 @@ Qed.
 Theorem spolynomial_simplify_ok :
  forall p:spolynomial, interp_cs (spolynomial_simplify p) = interp_sp p.
 intro.
-unfold spolynomial_simplify in |- *.
+unfold spolynomial_simplify.
 rewrite canonical_sum_simplify_ok.
 apply spolynomial_normalize_ok.
 Qed.
@@ -749,11 +745,11 @@ Qed.
 (* End properties. *)
 End semi_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SPconst.
-Implicit Arguments SPplus.
-Implicit Arguments SPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SPconst : default implicits.
+Arguments SPplus : default implicits.
+Arguments SPmult : default implicits.
 
 Section rings.
 
@@ -797,8 +793,7 @@ 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 refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 (*** Definitions *)
@@ -855,7 +850,7 @@ 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 in |- *; intros).
+simple induction p; reflexivity || (simpl; intros).
 rewrite H; rewrite H0; reflexivity.
 rewrite H; rewrite H0; reflexivity.
 rewrite H.
@@ -868,23 +863,23 @@ Theorem polynomial_normalize_ok :
  forall p:polynomial,
    polynomial_normalize p =
    spolynomial_normalize Aplus Amult Aone (spolynomial_of p).
-simple induction p; reflexivity || (simpl in |- *; intros).
+simple induction p; reflexivity || (simpl; intros).
 rewrite H; rewrite H0; reflexivity.
 rewrite H; rewrite H0; reflexivity.
-rewrite H; simpl in |- *.
+rewrite H; simpl.
 elim
  (canonical_sum_scalar3 Aplus Amult Aone (Aopp Aone) Nil_var
     (spolynomial_normalize Aplus Amult Aone (spolynomial_of p0)));
  [ reflexivity
- | simpl in |- *; intros; rewrite H0; reflexivity
- | simpl in |- *; intros; rewrite H0; 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 in |- *.
+unfold polynomial_simplify.
 rewrite spolynomial_of_ok.
 rewrite polynomial_normalize_ok.
 rewrite (canonical_sum_simplify_ok A Aplus Amult Aone Azero Aeq vm T).
diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v
index da4e3756..4717edc9 100644
--- a/plugins/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Setoid_ring_theory.
 Require Export Quote.
 Require Export Setoid_ring_normalize.
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index c4527cfb..b0d790e0 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -1,22 +1,19 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Import Setoid_ring_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
-  simple induction n; simple induction m; simpl in |- *;
+  simple induction n; simple induction m; simpl;
    try reflexivity || contradiction.
   intros; rewrite (H i0); trivial.
   intros; rewrite (H i0); trivial.
@@ -390,14 +387,13 @@ 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 refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+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 in |- *; intros.
+  simpl; intros.
   generalize (andb_prop2 _ _ H1); intros; elim H2; intros.
   rewrite (index_eq_prop _ _ H3); rewrite (H v0 H4); reflexivity.
 Qed.
@@ -406,7 +402,7 @@ 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 in |- *; intros.
+  simple induction v; simpl; intros.
   trivial.
   rewrite (H i); trivial.
 Qed.
@@ -416,17 +412,17 @@ Lemma varlist_merge_ok :
    Aequiv (interp_vl (varlist_merge x y)) (Amult (interp_vl x) (interp_vl y)).
 Proof.
   simple induction x.
-  simpl in |- *; trivial.
+  simpl; trivial.
   simple induction y.
-  simpl in |- *; trivial.
-  simpl in |- *; intros.
-  elim (index_lt i i0); simpl in |- *; intros.
+  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 in |- *.
+  simpl.
   rewrite (ivl_aux_ok v0 i0).
   eauto.
 
@@ -451,7 +447,7 @@ 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 in |- *; intros; trivial.
+ simple induction s; simpl; intros; trivial.
 Qed.
 
 Remark interp_m_ok :
@@ -471,16 +467,16 @@ Lemma canonical_sum_merge_ok :
    Aequiv (interp_setcs (canonical_sum_merge x y))
      (Aplus (interp_setcs x) (interp_setcs y)).
 Proof.
-simple induction x; simpl in |- *.
+simple induction x; simpl.
 trivial.
 
-simple induction y; simpl in |- *; intros.
+simple induction y; simpl; intros.
 eauto.
 
 generalize (varlist_eq_prop v v0).
 elim (varlist_eq v v0).
 intros; rewrite (H1 I).
-simpl in |- *.
+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)).
@@ -507,14 +503,14 @@ setoid_replace
  [ idtac | trivial ].
 auto.
 
-elim (varlist_lt v v0); simpl in |- *.
+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 in |- *.
+rewrite (H (Cons_monom a0 v0 c0)); simpl.
 rewrite (ics_aux_ok (interp_m a0 v0) c0); auto.
 
 intro.
@@ -540,13 +536,13 @@ rewrite
         end) c0)).
 rewrite H0.
 rewrite (ics_aux_ok (interp_m a v) c);
- rewrite (ics_aux_ok (interp_m a0 v0) c0); simpl in |- *;
+ 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 in |- *.
+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).
@@ -573,13 +569,13 @@ setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0);
  [ idtac | trivial ].
 auto.
 
-elim (varlist_lt v v0); simpl in |- *.
+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 in |- *.
+rewrite (H (Cons_varlist v0 c0)); simpl.
 rewrite (ics_aux_ok (interp_vl v0) c0).
 auto.
 
@@ -605,16 +601,16 @@ rewrite
              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 in |- *.
+ simpl.
 auto.
 
-simple induction y; simpl in |- *; intros.
+simple induction y; simpl; intros.
 trivial.
 
 generalize (varlist_eq_prop v v0).
 elim (varlist_eq v v0).
 intros; rewrite (H1 I).
-simpl in |- *.
+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).
@@ -638,12 +634,12 @@ setoid_replace
  [ idtac | trivial ].
 auto.
 
-elim (varlist_lt v v0); simpl in |- *; intros.
+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 in |- *.
+rewrite (H (Cons_monom a v0 c0)); simpl.
 rewrite (ics_aux_ok (interp_m a v0) c0); auto.
 
 rewrite
@@ -667,11 +663,11 @@ rewrite
              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 in |- *; auto.
+ simpl; auto.
 
 generalize (varlist_eq_prop v v0).
 elim (varlist_eq v v0); intros.
-rewrite (H1 I); simpl in |- *.
+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);
@@ -695,12 +691,12 @@ setoid_replace
 [ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v0)) with (interp_vl v0); auto.
 
-elim (varlist_lt v v0); simpl in |- *.
+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 in |- *.
+ simpl.
 rewrite (ics_aux_ok (interp_vl v0) c0); auto.
 
 rewrite
@@ -724,7 +720,7 @@ rewrite
              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 in |- *; auto.
+ simpl; auto.
 Qed.
 
 Lemma monom_insert_ok :
@@ -733,10 +729,10 @@ Lemma monom_insert_ok :
      (Aplus (Amult a (interp_vl l)) (interp_setcs s)).
 Proof.
 simple induction s; intros.
-simpl in |- *; rewrite (interp_m_ok a l); trivial.
+simpl; rewrite (interp_m_ok a l); trivial.
 
-simpl in |- *; generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *.
+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).
@@ -745,7 +741,7 @@ setoid_replace (Amult (Aplus a a0) (interp_vl v)) with
  [ idtac | trivial ].
 auto.
 
-elim (varlist_lt l v); simpl in |- *; intros.
+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.
@@ -754,9 +750,9 @@ 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 in |- *.
+simpl.
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *.
+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).
@@ -767,7 +763,7 @@ setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v);
  [ idtac | trivial ].
 auto.
 
-elim (varlist_lt l v); simpl in |- *; intros; 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.
@@ -777,11 +773,11 @@ Lemma varlist_insert_ok :
    Aequiv (interp_setcs (varlist_insert l s))
      (Aplus (interp_vl l) (interp_setcs s)).
 Proof.
-simple induction s; simpl in |- *; intros.
+simple induction s; simpl; intros.
 trivial.
 
 generalize (varlist_eq_prop l v); elim (varlist_eq l v).
-intro Hr; rewrite (Hr I); simpl in |- *.
+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).
@@ -790,14 +786,14 @@ setoid_replace (Amult (Aplus Aone a) (interp_vl v)) with
  [ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
-elim (varlist_lt l v); simpl in |- *; intros; 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 in |- *.
+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).
@@ -806,7 +802,7 @@ setoid_replace (Amult (Aplus Aone Aone) (interp_vl v)) with
  [ idtac | trivial ].
 setoid_replace (Amult Aone (interp_vl v)) with (interp_vl v); auto.
 
-elim (varlist_lt l v); simpl in |- *; intros; 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.
@@ -817,7 +813,7 @@ Lemma canonical_sum_scalar_ok :
    Aequiv (interp_setcs (canonical_sum_scalar a s))
      (Amult a (interp_setcs s)).
 Proof.
-simple induction s; simpl in |- *; intros.
+simple induction s; simpl; intros.
 trivial.
 
 rewrite (ics_aux_ok (interp_m (Amult a a0) v) (canonical_sum_scalar a c));
@@ -840,7 +836,7 @@ Lemma canonical_sum_scalar2_ok :
    Aequiv (interp_setcs (canonical_sum_scalar2 l s))
      (Amult (interp_vl l) (interp_setcs s)).
 Proof.
-simple induction s; simpl in |- *; intros; auto.
+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).
@@ -865,7 +861,7 @@ Lemma canonical_sum_scalar3_ok :
    Aequiv (interp_setcs (canonical_sum_scalar3 c l s))
      (Amult c (Amult (interp_vl l) (interp_setcs s))).
 Proof.
-simple induction s; simpl in |- *; intros.
+simple induction s; simpl; intros.
 rewrite (SSR_mult_zero_right S T (interp_vl l)).
 auto.
 
@@ -914,7 +910,7 @@ Lemma canonical_sum_prod_ok :
    Aequiv (interp_setcs (canonical_sum_prod x y))
      (Amult (interp_setcs x) (interp_setcs y)).
 Proof.
-simple induction x; simpl in |- *; intros.
+simple induction x; simpl; intros.
 trivial.
 
 rewrite
@@ -948,7 +944,7 @@ Theorem setspolynomial_normalize_ok :
  forall p:setspolynomial,
    Aequiv (interp_setcs (setspolynomial_normalize p)) (interp_setsp p).
 Proof.
-simple induction p; simpl in |- *; intros; trivial.
+simple induction p; simpl; intros; trivial.
 rewrite
  (canonical_sum_merge_ok (setspolynomial_normalize s)
     (setspolynomial_normalize s0)).
@@ -964,12 +960,12 @@ Lemma canonical_sum_simplify_ok :
  forall s:canonical_sum,
    Aequiv (interp_setcs (canonical_sum_simplify s)) (interp_setcs s).
 Proof.
-simple induction s; simpl in |- *; intros.
+simple induction s; simpl; intros.
 trivial.
 
 generalize (SSR_eq_prop T a Azero).
 elim (Aeq a Azero).
-simpl in |- *.
+simpl.
 intros.
 rewrite (ics_aux_ok (interp_m a v) c).
 rewrite (interp_m_ok a v).
@@ -979,19 +975,19 @@ setoid_replace (Amult Azero (interp_vl v)) with Azero;
 rewrite H.
 trivial.
 
-intros; simpl in |- *.
+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 in |- *.
+simpl.
 rewrite (ics_aux_ok (interp_vl v) (canonical_sum_simplify c)).
 rewrite H.
 auto.
 
-simpl in |- *.
+simpl.
 intros.
 rewrite (ics_aux_ok (interp_m a v) (canonical_sum_simplify c)).
 rewrite (ics_aux_ok (interp_m a v) c).
@@ -1007,18 +1003,18 @@ Theorem setspolynomial_simplify_ok :
    Aequiv (interp_setcs (setspolynomial_simplify p)) (interp_setsp p).
 Proof.
 intro.
-unfold setspolynomial_simplify in |- *.
+unfold setspolynomial_simplify.
 rewrite (canonical_sum_simplify_ok (setspolynomial_normalize p)).
 exact (setspolynomial_normalize_ok p).
 Qed.
 
 End semi_setoid_rings.
 
-Implicit Arguments Cons_varlist.
-Implicit Arguments Cons_monom.
-Implicit Arguments SetSPconst.
-Implicit Arguments SetSPplus.
-Implicit Arguments SetSPmult.
+Arguments Cons_varlist : default implicits.
+Arguments Cons_monom : default implicits.
+Arguments SetSPconst : default implicits.
+Arguments SetSPplus : default implicits.
+Arguments SetSPmult : default implicits.
 
 
 
@@ -1055,8 +1051,7 @@ 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 refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 
@@ -1113,7 +1108,7 @@ 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 in |- *; intros.
+simple induction p; trivial; simpl; intros.
 rewrite H; rewrite H0; trivial.
 rewrite H; rewrite H0; trivial.
 rewrite H.
@@ -1127,23 +1122,23 @@ Qed.
 Theorem setpolynomial_normalize_ok :
  forall p:setpolynomial,
    setpolynomial_normalize p = setspolynomial_normalize (setspolynomial_of p).
-simple induction p; trivial; simpl in |- *; intros.
+simple induction p; trivial; simpl; intros.
 rewrite H; rewrite H0; reflexivity.
 rewrite H; rewrite H0; reflexivity.
-rewrite H; simpl in |- *.
+rewrite H; simpl.
 elim
  (canonical_sum_scalar3 (Aopp Aone) Nil_var
     (setspolynomial_normalize (setspolynomial_of s)));
  [ reflexivity
- | simpl in |- *; intros; rewrite H0; reflexivity
- | simpl in |- *; intros; rewrite H0; 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 in |- *.
+unfold setpolynomial_simplify.
 rewrite (setspolynomial_of_ok p).
 rewrite setpolynomial_normalize_ok.
 rewrite
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
index f07cbaf6..52f5968b 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Setoid_ring_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 Require Export Bool.
 Require Export Setoid.
 
@@ -408,7 +406,7 @@ Unset Implicit Arguments.
 Definition Semi_Setoid_Ring_Theory_of :
   Setoid_Ring_Theory -> Semi_Setoid_Ring_Theory.
 intros until 1; case H.
-split; intros; simpl in |- *; eauto.
+split; intros; simpl; eauto.
 Defined.
 
 Coercion Semi_Setoid_Ring_Theory_of : Setoid_Ring_Theory >->
diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
index c5a33f39..8953b88f 100644
--- a/plugins/ring/g_ring.ml4
+++ b/plugins/ring/g_ring.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_ring.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 open Quote
 open Ring
 open Tacticals
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 6e67272c..7b0d96bb 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ring.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (* ML part of the Ring tactic *)
 
 open Pp
@@ -21,7 +19,6 @@ open Reductionops
 open Tacticals
 open Tacexpr
 open Tacmach
-open Proof_trees
 open Printer
 open Equality
 open Vernacinterp
@@ -138,7 +135,7 @@ let mkLApp(fc,v) = mkApp(Lazy.force fc, v)
 module OperSet =
   Set.Make (struct
 	      type t = global_reference
-	      let compare = (Pervasives.compare : t->t->int)
+	      let compare = (RefOrdered.compare : t->t->int)
 	    end)
 
 type morph =
@@ -169,7 +166,7 @@ type theory =
 (* Theories are stored in a table which is synchronised with the Reset
    mechanism. *)
 
-module Cmap = Map.Make(struct type t = constr let compare = compare end)
+module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
 
 let theories_map = ref Cmap.empty
 
@@ -265,7 +262,7 @@ let subst_th (subst,(c,th as obj)) =
       (c',th')
 
 
-let (theory_to_obj, obj_to_theory) =
+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);
@@ -295,7 +292,8 @@ let unbox = function
 (* 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
+let safe_pf_conv_x gl c1 c2 =
+  try pf_conv_x gl c1 c2 with e when Errors.noncritical e -> false
 
 
 (* Add a Ring or a Semi-Ring to the database after a type verification *)
@@ -380,8 +378,14 @@ Builds
 
 *)
 
+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  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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
@@ -395,14 +399,14 @@ let build_spolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SPconst, [|th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash 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;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -437,7 +441,7 @@ Builds
 *)
 
 let build_polynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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 =
@@ -446,7 +450,7 @@ let build_polynom gl th lc =
 	  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 Zminus *)
+      (* 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|])|])) ->
@@ -458,14 +462,14 @@ let build_polynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_Pconst, [|th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash 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;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -501,7 +505,7 @@ Builds
 *)
 
 let build_aspolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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
@@ -515,13 +519,13 @@ let build_aspolynom gl th lc =
       | _ 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 Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar = mkLApp(coq_ASPvar, [|(path_of_int !counter) |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -555,7 +559,7 @@ Builds
 *)
 
 let build_apolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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 =
@@ -564,7 +568,7 @@ let build_apolynom gl th lc =
 	  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 Zminus *)
+      (* 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|]) |])) ->
@@ -575,14 +579,14 @@ let build_apolynom gl th lc =
       | _ 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 Hashtbl.find varhash c
+	  try Constrhash.find varhash c
 	  with Not_found ->
 	    let newvar =
               mkLApp(coq_APvar, [| path_of_int !counter |]) in
 	    begin
 	      incr counter;
 	      varlist := c :: !varlist;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -616,7 +620,7 @@ Builds
 *)
 
 let build_setpolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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 =
@@ -625,7 +629,7 @@ let build_setpolynom gl th lc =
 	  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 Zminus *)
+      (* 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|])|])) ->
@@ -637,14 +641,14 @@ let build_setpolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SetPconst, [| th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash 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;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -683,7 +687,7 @@ Builds
 *)
 
 let build_setspolynom gl th lc =
-  let varhash  = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in
+  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 =
@@ -695,14 +699,14 @@ let build_setspolynom gl th lc =
       | _ when closed_under th.th_closed c ->
 	  mkLApp(coq_SetSPconst, [| th.th_a; c |])
       | _ ->
-	  try Hashtbl.find varhash 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;
-	      Hashtbl.add varhash c newvar;
+	      Constrhash.add varhash c newvar;
 	      newvar
 	    end
   in
@@ -823,9 +827,9 @@ let raw_polynom th op lc gl =
 	      (tclTHENS
 		 (tclORELSE
                    (Equality.general_rewrite true
-		     Termops.all_occurrences false c'i_eq_c''i)
+		     Termops.all_occurrences true false c'i_eq_c''i)
                    (Equality.general_rewrite false
-		     Termops.all_occurrences false c'i_eq_c''i))
+		     Termops.all_occurrences true false c'i_eq_c''i))
                  [tac]))
 	 else
            (tclORELSE