Kills the useless tactic annotations "in |- *"

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

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

7 files changed, 190 insertions, 190 deletions

diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 94dc48a733..9c059cea17 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -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/LegacyRing.v b/plugins/ring/LegacyRing.v
index d19e9f589a..132014331b 100644
--- a/plugins/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
@@ -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 ca3355a6ec..d0bc46ea48 100644
--- a/plugins/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
@@ -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/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index 5358941605..7995696ffb 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -143,7 +143,7 @@ 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.
@@ -158,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.
@@ -177,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 :
@@ -192,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.
@@ -208,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.
@@ -451,7 +451,7 @@ 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.
@@ -460,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.
 
@@ -476,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.
@@ -497,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.
@@ -516,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 :
@@ -528,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.
@@ -555,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.
@@ -568,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.
 
@@ -579,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.
@@ -605,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).
@@ -629,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.
@@ -642,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).
@@ -662,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.
@@ -685,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 9755d71e12..0d8393f76b 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -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.
 
@@ -371,7 +371,7 @@ 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.
@@ -380,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.
@@ -390,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.
 
@@ -410,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.
@@ -420,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.
 
@@ -428,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.
 
@@ -439,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).
@@ -465,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.
 
@@ -479,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).
@@ -487,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).
@@ -505,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.
 
@@ -518,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 ].
@@ -546,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 ].
@@ -573,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.
@@ -583,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.
@@ -596,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.
@@ -610,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.
@@ -627,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.
@@ -641,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.
@@ -657,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.
@@ -666,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.
@@ -678,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.
@@ -699,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).
@@ -709,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.
@@ -737,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.
@@ -850,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.
@@ -863,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_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index 94b36e2467..59d86cede7 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -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.
@@ -393,7 +393,7 @@ 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.
@@ -402,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.
@@ -412,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.
 
@@ -447,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 :
@@ -467,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)).
@@ -503,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.
@@ -536,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).
@@ -569,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.
 
@@ -601,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).
@@ -634,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
@@ -663,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);
@@ -691,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
@@ -720,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 :
@@ -729,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).
@@ -741,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.
@@ -750,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).
@@ -763,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.
@@ -773,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).
@@ -786,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).
@@ -802,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.
@@ -813,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));
@@ -836,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).
@@ -861,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.
 
@@ -910,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
@@ -944,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)).
@@ -960,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).
@@ -975,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).
@@ -1003,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.
@@ -1108,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.
@@ -1122,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 dd722f8011..870fe40f1c 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -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 >->