Imported Upstream version 8.4dfsgupstream/8.4dfsg

12 files changed, 226 insertions, 233 deletions

diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index fd5bcd93..089dec02 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -13,7 +13,7 @@ Require Export LegacyRing.
 Require Export Arith.
 Require Import Eqdep_dec.
 
-Open Local Scope nat_scope.
+Local Open Scope nat_scope.
 
 Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
@@ -75,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 5dcd6d84..7f1597a1 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -22,23 +22,22 @@ 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 d19e9f58..d4f40081 100644
--- a/plugins/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -19,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.
@@ -28,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 ca3355a6..09de1bb4 100644
--- a/plugins/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -58,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.
@@ -100,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.
@@ -176,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.
@@ -214,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.
@@ -233,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.
@@ -255,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.
@@ -306,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)).
@@ -342,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.
@@ -357,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 5845062d..3f01a5c3 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -21,15 +21,15 @@ 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 1763d70a..a00b7bcd 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -137,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.
@@ -159,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.
@@ -178,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 :
@@ -193,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.
@@ -209,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.
@@ -446,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.
@@ -462,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.
 
@@ -478,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.
@@ -499,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.
@@ -518,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 :
@@ -530,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.
@@ -557,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.
@@ -570,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.
 
@@ -581,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.
@@ -607,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).
@@ -631,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.
@@ -644,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).
@@ -664,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.
@@ -687,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 c6dff3e0..d286208a 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -16,7 +16,7 @@ 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.
 
@@ -365,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.
@@ -381,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.
@@ -391,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.
 
@@ -411,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.
@@ -421,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.
 
@@ -429,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.
 
@@ -440,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).
@@ -466,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.
 
@@ -480,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).
@@ -488,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).
@@ -506,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.
 
@@ -519,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 ].
@@ -547,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 ].
@@ -574,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.
@@ -584,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.
@@ -597,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.
@@ -611,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.
@@ -628,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.
@@ -642,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.
@@ -658,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.
@@ -667,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.
@@ -679,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.
@@ -700,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).
@@ -710,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.
@@ -738,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.
@@ -794,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 *)
@@ -852,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.
@@ -865,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 106a946d..4717edc9 100644
--- a/plugins/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index ad75a8a4..b0d790e0 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -13,7 +13,7 @@ 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 in |- *;
+  simple induction n; simple induction m; simpl;
    try reflexivity || contradiction.
   intros; rewrite (H i0); trivial.
   intros; rewrite (H i0); trivial.
@@ -387,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.
@@ -403,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.
@@ -413,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.
 
@@ -448,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 :
@@ -468,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)).
@@ -504,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.
@@ -537,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).
@@ -570,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.
 
@@ -602,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).
@@ -635,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
@@ -664,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);
@@ -692,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
@@ -721,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 :
@@ -730,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).
@@ -742,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.
@@ -751,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).
@@ -764,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.
@@ -774,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).
@@ -787,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).
@@ -803,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.
@@ -814,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));
@@ -837,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).
@@ -862,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.
 
@@ -911,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
@@ -945,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)).
@@ -961,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).
@@ -976,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).
@@ -1004,7 +1003,7 @@ 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.
@@ -1052,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.
 
 
@@ -1110,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.
@@ -1124,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 dd722f80..52f5968b 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -406,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 e306a531..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-2010     *)
+(* <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        *)
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 98d6361c..ae73069d 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <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        *)
@@ -449,7 +449,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|])|])) ->
@@ -567,7 +567,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|]) |])) ->
@@ -628,7 +628,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|])|])) ->