From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/Reals/RList.v | 232 ++++++++++++++++++++++++-------------------------
 1 file changed, 116 insertions(+), 116 deletions(-)

(limited to 'theories/Reals/RList.v')

diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v
index dbd2e52f..6d42434a 100644
--- a/theories/Reals/RList.v
+++ b/theories/Reals/RList.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        *)
@@ -8,7 +8,7 @@
 
 Require Import Rbase.
 Require Import Rfunctions.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
 Inductive Rlist : Type :=
 | nil : Rlist
@@ -52,19 +52,19 @@ Proof.
   simpl in H; elim H.
   induction  l as [| r0 l Hrecl0].
   simpl in H; elim H; intro.
-  simpl in |- *; right; assumption.
+  simpl; right; assumption.
   elim H0.
   replace (MaxRlist (cons r (cons r0 l))) with (Rmax r (MaxRlist (cons r0 l))).
   simpl in H; decompose [or] H.
   rewrite H0; apply RmaxLess1.
-  unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
-  apply Hrecl; simpl in |- *; tauto.
+  unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+  apply Hrecl; simpl; tauto.
   apply Rle_trans with (MaxRlist (cons r0 l));
-    [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
-  unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
-  apply Hrecl; simpl in |- *; tauto.
+    [ apply Hrecl; simpl; tauto | left; auto with real ].
+  unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l))); intro.
+  apply Hrecl; simpl; tauto.
   apply Rle_trans with (MaxRlist (cons r0 l));
-    [ apply Hrecl; simpl in |- *; tauto | left; auto with real ].
+    [ apply Hrecl; simpl; tauto | left; auto with real ].
   reflexivity.
 Qed.
 
@@ -80,19 +80,19 @@ Proof.
   simpl in H; elim H.
   induction  l as [| r0 l Hrecl0].
   simpl in H; elim H; intro.
-  simpl in |- *; right; symmetry  in |- *; assumption.
+  simpl; right; symmetry ; assumption.
   elim H0.
   replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
   simpl in H; decompose [or] H.
   rewrite H0; apply Rmin_l.
-  unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
+  unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro.
   apply Rle_trans with (MinRlist (cons r0 l)).
   assumption.
-  apply Hrecl; simpl in |- *; tauto.
-  apply Hrecl; simpl in |- *; tauto.
+  apply Hrecl; simpl; tauto.
+  apply Hrecl; simpl; tauto.
   apply Rle_trans with (MinRlist (cons r0 l)).
   apply Rmin_r.
-  apply Hrecl; simpl in |- *; tauto.
+  apply Hrecl; simpl; tauto.
   reflexivity.
 Qed.
 
@@ -101,7 +101,7 @@ Lemma AbsList_P1 :
 Proof.
   intros; induction  l as [| r l Hrecl].
   elim H.
-  simpl in |- *; simpl in H; elim H; intro.
+  simpl; simpl in H; elim H; intro.
   left; rewrite H0; reflexivity.
   right; apply Hrecl; assumption.
 Qed.
@@ -112,11 +112,11 @@ Proof.
   intros; induction  l as [| r l Hrecl].
   apply Rlt_0_1.
   induction  l as [| r0 l Hrecl0].
-  simpl in |- *; apply H; simpl in |- *; tauto.
+  simpl; apply H; simpl; tauto.
   replace (MinRlist (cons r (cons r0 l))) with (Rmin r (MinRlist (cons r0 l))).
-  unfold Rmin in |- *; case (Rle_dec r (MinRlist (cons r0 l))); intro.
-  apply H; simpl in |- *; tauto.
-  apply Hrecl; intros; apply H; simpl in |- *; simpl in H0; tauto.
+  unfold Rmin; case (Rle_dec r (MinRlist (cons r0 l))); intro.
+  apply H; simpl; tauto.
+  apply Hrecl; intros; apply H; simpl; simpl in H0; tauto.
   reflexivity.
 Qed.
 
@@ -128,10 +128,10 @@ Proof.
   elim H.
   elim H; intro.
   exists r; split.
-  simpl in |- *; tauto.
+  simpl; tauto.
   assumption.
   assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros;
-    exists x0; simpl in |- *; simpl in H2; tauto.
+    exists x0; simpl; simpl in H2; tauto.
 Qed.
 
 Lemma MaxRlist_P2 :
@@ -140,9 +140,9 @@ Proof.
   intros; induction  l as [| r l Hrecl].
   simpl in H; elim H; trivial.
   induction  l as [| r0 l Hrecl0].
-  simpl in |- *; left; reflexivity.
-  change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l))) in |- *;
-    unfold Rmax in |- *; case (Rle_dec r (MaxRlist (cons r0 l)));
+  simpl; left; reflexivity.
+  change (In (Rmax r (MaxRlist (cons r0 l))) (cons r (cons r0 l)));
+    unfold Rmax; case (Rle_dec r (MaxRlist (cons r0 l)));
       intro.
   right; apply Hrecl; exists r0; left; reflexivity.
   left; reflexivity.
@@ -164,7 +164,7 @@ Lemma pos_Rl_P1 :
 Proof.
   intros; induction  l as [| r l Hrecl];
     [ elim (lt_n_O _ H)
-      | simpl in |- *; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
+      | simpl; case (Rlength l); [ reflexivity | intro; reflexivity ] ].
 Qed.
 
 Lemma pos_Rl_P2 :
@@ -177,14 +177,14 @@ Proof.
   split; intro.
   elim H; intro.
   exists 0%nat; split;
-    [ simpl in |- *; apply lt_O_Sn | simpl in |- *; apply H0 ].
+    [ simpl; apply lt_O_Sn | simpl; apply H0 ].
   elim Hrecl; intros; assert (H3 := H1 H0); elim H3; intros; elim H4; intros;
     exists (S x0); split;
-      [ simpl in |- *; apply lt_n_S; assumption | simpl in |- *; assumption ].
+      [ simpl; apply lt_n_S; assumption | simpl; assumption ].
   elim H; intros; elim H0; intros; elim (zerop x0); intro.
   rewrite a in H2; simpl in H2; left; assumption.
   right; elim Hrecl; intros; apply H4; assert (H5 : S (pred x0) = x0).
-  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  symmetry ; apply S_pred with 0%nat; assumption.
   exists (pred x0); split;
     [ simpl in H1; apply lt_S_n; rewrite H5; assumption
       | rewrite <- H5 in H2; simpl in H2; assumption ].
@@ -201,18 +201,18 @@ Proof.
   exists nil; intros; split;
     [ reflexivity | intros; simpl in H0; elim (lt_n_O _ H0) ].
   assert (H0 : In r (cons r l)).
-  simpl in |- *; left; reflexivity.
+  simpl; left; reflexivity.
   assert (H1 := H _ H0);
     assert (H2 : forall x:R, In x l ->  exists y : R, P x y).
-  intros; apply H; simpl in |- *; right; assumption.
+  intros; apply H; simpl; right; assumption.
   assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (cons x x0);
     intros; elim H5; clear H5; intros; split.
-  simpl in |- *; rewrite H5; reflexivity.
+  simpl; rewrite H5; reflexivity.
   intros; elim (zerop i); intro.
-  rewrite a; simpl in |- *; assumption.
+  rewrite a; simpl; assumption.
   assert (H8 : i = S (pred i)).
   apply S_pred with 0%nat; assumption.
-  rewrite H8; simpl in |- *; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
+  rewrite H8; simpl; apply H6; simpl in H7; apply lt_S_n; rewrite <- H8;
     assumption.
 Qed.
 
@@ -271,7 +271,7 @@ Lemma RList_P0 :
 Proof.
   intros; induction  l as [| r l Hrecl];
     [ left; reflexivity
-      | simpl in |- *; case (Rle_dec r a); intro;
+      | simpl; case (Rle_dec r a); intro;
         [ right; reflexivity | left; reflexivity ] ].
 Qed.
 
@@ -279,41 +279,41 @@ Lemma RList_P1 :
   forall (l:Rlist) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).
 Proof.
   intros; induction  l as [| r l Hrecl].
-  simpl in |- *; unfold ordered_Rlist in |- *; intros; simpl in H0;
+  simpl; unfold ordered_Rlist; intros; simpl in H0;
     elim (lt_n_O _ H0).
-  simpl in |- *; case (Rle_dec r a); intro.
+  simpl; case (Rle_dec r a); intro.
   assert (H1 : ordered_Rlist l).
-  unfold ordered_Rlist in |- *; unfold ordered_Rlist in H; intros;
+  unfold ordered_Rlist; unfold ordered_Rlist in H; intros;
     assert (H1 : (S i < pred (Rlength (cons r l)))%nat);
-      [ simpl in |- *; replace (Rlength l) with (S (pred (Rlength l)));
+      [ simpl; replace (Rlength l) with (S (pred (Rlength l)));
         [ apply lt_n_S; assumption
-          | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
+          | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
             intro; rewrite <- H1 in H0; simpl in H0; elim (lt_n_O _ H0) ]
         | apply (H _ H1) ].
-  assert (H2 := Hrecl H1); unfold ordered_Rlist in |- *; intros;
+  assert (H2 := Hrecl H1); unfold ordered_Rlist; intros;
     induction  i as [| i Hreci].
-  simpl in |- *; assert (H3 := RList_P0 l a); elim H3; intro.
+  simpl; assert (H3 := RList_P0 l a); elim H3; intro.
   rewrite H4; assumption.
   induction  l as [| r1 l Hrecl0];
-    [ simpl in |- *; assumption
-      | rewrite H4; apply (H 0%nat); simpl in |- *; apply lt_O_Sn ].
-  simpl in |- *; apply H2; simpl in H0; apply lt_S_n;
+    [ simpl; assumption
+      | rewrite H4; apply (H 0%nat); simpl; apply lt_O_Sn ].
+  simpl; apply H2; simpl in H0; apply lt_S_n;
     replace (S (pred (Rlength (insert l a)))) with (Rlength (insert l a));
     [ assumption
-      | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
+      | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
         rewrite <- H3 in H0; elim (lt_n_O _ H0) ].
-  unfold ordered_Rlist in |- *; intros; induction  i as [| i Hreci];
-    [ simpl in |- *; auto with real
-      | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)) in |- *; apply H;
-        simpl in H0; simpl in |- *; apply (lt_S_n _ _ H0) ].
+  unfold ordered_Rlist; intros; induction  i as [| i Hreci];
+    [ simpl; auto with real
+      | change (pos_Rl (cons r l) i <= pos_Rl (cons r l) (S i)); apply H;
+        simpl in H0; simpl; apply (lt_S_n _ _ H0) ].
 Qed.
 
 Lemma RList_P2 :
   forall l1 l2:Rlist, ordered_Rlist l2 -> ordered_Rlist (cons_ORlist l1 l2).
 Proof.
   simple induction l1;
-    [ intros; simpl in |- *; apply H
-      | intros; simpl in |- *; apply H; apply RList_P1; assumption ].
+    [ intros; simpl; apply H
+      | intros; simpl; apply H; apply RList_P1; assumption ].
 Qed.
 
 Lemma RList_P3 :
@@ -324,11 +324,11 @@ Proof.
     [ induction  l as [| r l Hrecl] | induction  l as [| r l Hrecl] ].
   elim H.
   elim H; intro;
-    [ exists 0%nat; split; [ apply H0 | simpl in |- *; apply lt_O_Sn ]
+    [ exists 0%nat; split; [ apply H0 | simpl; apply lt_O_Sn ]
       | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split;
-        [ apply H1 | simpl in |- *; apply lt_n_S; assumption ] ].
+        [ apply H1 | simpl; apply lt_n_S; assumption ] ].
   elim H; intros; elim H0; intros; elim (lt_n_O _ H2).
-  simpl in |- *; elim H; intros; elim H0; clear H0; intros;
+  simpl; elim H; intros; elim H0; clear H0; intros;
     induction  x0 as [| x0 Hrecx0];
       [ left; apply H0
         | right; apply Hrecl; exists x0; split;
@@ -338,10 +338,10 @@ Qed.
 Lemma RList_P4 :
   forall (l1:Rlist) (a:R), ordered_Rlist (cons a l1) -> ordered_Rlist l1.
 Proof.
-  intros; unfold ordered_Rlist in |- *; intros; apply (H (S i)); simpl in |- *;
+  intros; unfold ordered_Rlist; intros; apply (H (S i)); simpl;
     replace (Rlength l1) with (S (pred (Rlength l1)));
     [ apply lt_n_S; assumption
-      | symmetry  in |- *; apply S_pred with 0%nat; apply neq_O_lt; red in |- *;
+      | symmetry ; apply S_pred with 0%nat; apply neq_O_lt; red;
         intro; rewrite <- H1 in H0; elim (lt_n_O _ H0) ].
 Qed.
 
@@ -350,11 +350,11 @@ Lemma RList_P5 :
 Proof.
   intros; induction  l as [| r l Hrecl];
     [ elim H0
-      | simpl in |- *; elim H0; intro;
+      | simpl; elim H0; intro;
         [ rewrite H1; right; reflexivity
           | apply Rle_trans with (pos_Rl l 0);
-            [ apply (H 0%nat); simpl in |- *; induction  l as [| r0 l Hrecl0];
-              [ elim H1 | simpl in |- *; apply lt_O_Sn ]
+            [ apply (H 0%nat); simpl; induction  l as [| r0 l Hrecl0];
+              [ elim H1 | simpl; apply lt_O_Sn ]
               | apply Hrecl; [ eapply RList_P4; apply H | assumption ] ] ] ].
 Qed.
 
@@ -366,13 +366,13 @@ Lemma RList_P6 :
 Proof.
   simple induction l; split; intro.
   intros; right; reflexivity.
-  unfold ordered_Rlist in |- *; intros; simpl in H0; elim (lt_n_O _ H0).
+  unfold ordered_Rlist; intros; simpl in H0; elim (lt_n_O _ H0).
   intros; induction  i as [| i Hreci];
     [ induction  j as [| j Hrecj];
       [ right; reflexivity
-        | simpl in |- *; apply Rle_trans with (pos_Rl r0 0);
-          [ apply (H0 0%nat); simpl in |- *; simpl in H2; apply neq_O_lt;
-            red in |- *; intro; rewrite <- H3 in H2;
+        | simpl; apply Rle_trans with (pos_Rl r0 0);
+          [ apply (H0 0%nat); simpl; simpl in H2; apply neq_O_lt;
+            red; intro; rewrite <- H3 in H2;
               assert (H4 := lt_S_n _ _ H2); elim (lt_n_O _ H4)
             | elim H; intros; apply H3;
               [ apply RList_P4 with r; assumption
@@ -380,12 +380,12 @@ Proof.
                 | simpl in H2; apply lt_S_n; assumption ] ] ]
       | induction  j as [| j Hrecj];
         [ elim (le_Sn_O _ H1)
-          | simpl in |- *; elim H; intros; apply H3;
+          | simpl; elim H; intros; apply H3;
             [ apply RList_P4 with r; assumption
               | apply le_S_n; assumption
               | simpl in H2; apply lt_S_n; assumption ] ] ].
-  unfold ordered_Rlist in |- *; intros; apply H0;
-    [ apply le_n_Sn | simpl in |- *; simpl in H1; apply lt_n_S; assumption ].
+  unfold ordered_Rlist; intros; apply H0;
+    [ apply le_n_Sn | simpl; simpl in H1; apply lt_n_S; assumption ].
 Qed.
 
 Lemma RList_P7 :
@@ -397,11 +397,11 @@ Proof.
       clear H1; intros; assert (H4 := H1 H0); elim H4; clear H4;
         intros; elim H4; clear H4; intros; rewrite H4;
           assert (H6 : Rlength l = S (pred (Rlength l))).
-  apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
+  apply S_pred with 0%nat; apply neq_O_lt; red; intro;
     rewrite <- H6 in H5; elim (lt_n_O _ H5).
   apply H3;
     [ rewrite H6 in H5; apply lt_n_Sm_le; assumption
-      | apply lt_pred_n_n; apply neq_O_lt; red in |- *; intro; rewrite <- H7 in H5;
+      | apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H7 in H5;
         elim (lt_n_O _ H5) ].
 Qed.
 
@@ -420,7 +420,7 @@ Proof.
           [ left; assumption
             | right; left; assumption
             | right; right; assumption ] ]
-      | simpl in |- *; case (Rle_dec r a); intro;
+      | simpl; case (Rle_dec r a); intro;
         [ simpl in H0; decompose [or] H0;
           [ right; elim (H a x); intros; apply H3; left
             | left
@@ -435,14 +435,14 @@ Proof.
   simple induction l1.
   intros; split; intro;
     [ simpl in H; right; assumption
-      | simpl in |- *; elim H; intro; [ elim H0 | assumption ] ].
+      | simpl; elim H; intro; [ elim H0 | assumption ] ].
   intros; split.
-  simpl in |- *; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0);
+  simpl; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0);
     elim H3; intro;
       [ left; right; assumption
         | elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro;
           [ left; left; assumption | right; assumption ] ].
-  intro; simpl in |- *; elim (H (insert l2 r) x); intros _ H1; apply H1;
+  intro; simpl; elim (H (insert l2 r) x); intros _ H1; apply H1;
     elim H0; intro;
       [ elim H2; intro;
         [ right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left; assumption
@@ -455,8 +455,8 @@ Lemma RList_P10 :
 Proof.
   intros; induction  l as [| r l Hrecl];
     [ reflexivity
-      | simpl in |- *; case (Rle_dec r a); intro;
-        [ simpl in |- *; rewrite Hrecl; reflexivity | reflexivity ] ].
+      | simpl; case (Rle_dec r a); intro;
+        [ simpl; rewrite Hrecl; reflexivity | reflexivity ] ].
 Qed.
 
 Lemma RList_P11 :
@@ -465,7 +465,7 @@ Lemma RList_P11 :
 Proof.
   simple induction l1;
     [ intro; reflexivity
-      | intros; simpl in |- *; rewrite (H (insert l2 r)); rewrite RList_P10;
+      | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10;
         apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
           rewrite S_INR; ring ].
 Qed.
@@ -477,7 +477,7 @@ Proof.
   simple induction l;
     [ intros; elim (lt_n_O _ H)
       | intros; induction  i as [| i Hreci];
-        [ reflexivity | simpl in |- *; apply H; apply lt_S_n; apply H0 ] ].
+        [ reflexivity | simpl; apply H; apply lt_S_n; apply H0 ] ].
 Qed.
 
 Lemma RList_P13 :
@@ -494,13 +494,13 @@ Proof.
   change
     (pos_Rl (mid_Rlist (cons r1 r2) r) (S i) =
       (pos_Rl (cons r1 r2) i + pos_Rl (cons r1 r2) (S i)) / 2)
-    in |- *; apply H0; simpl in |- *; apply lt_S_n; assumption.
+   ; apply H0; simpl; apply lt_S_n; assumption.
 Qed.
 
 Lemma RList_P14 : forall (l:Rlist) (a:R), Rlength (mid_Rlist l a) = Rlength l.
 Proof.
   simple induction l; intros;
-    [ reflexivity | simpl in |- *; rewrite (H r); reflexivity ].
+    [ reflexivity | simpl; rewrite (H r); reflexivity ].
 Qed.
 
 Lemma RList_P15 :
@@ -511,7 +511,7 @@ Lemma RList_P15 :
 Proof.
   intros; apply Rle_antisym.
   induction  l1 as [| r l1 Hrecl1];
-    [ simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption
+    [ simpl; simpl in H1; right; symmetry ; assumption
       | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) 0)); intros;
         assert
           (H4 :
@@ -520,7 +520,7 @@ Proof.
             | assert (H5 := H3 H4); apply RList_P5;
               [ apply RList_P2; assumption | assumption ] ] ].
   induction  l1 as [| r l1 Hrecl1];
-    [ simpl in |- *; simpl in H1; right; assumption
+    [ simpl; simpl in H1; right; assumption
       | assert
         (H2 :
           In (pos_Rl (cons_ORlist (cons r l1) l2) 0) (cons_ORlist (cons r l1) l2));
@@ -528,7 +528,7 @@ Proof.
           (RList_P3 (cons_ORlist (cons r l1) l2)
             (pos_Rl (cons_ORlist (cons r l1) l2) 0));
           intros; apply H3; exists 0%nat; split;
-            [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_O_Sn ]
+            [ reflexivity | rewrite RList_P11; simpl; apply lt_O_Sn ]
           | elim (RList_P9 (cons r l1) l2 (pos_Rl (cons_ORlist (cons r l1) l2) 0));
             intros; assert (H5 := H3 H2); elim H5; intro;
               [ apply RList_P5; assumption
@@ -545,7 +545,7 @@ Lemma RList_P16 :
 Proof.
   intros; apply Rle_antisym.
   induction  l1 as [| r l1 Hrecl1].
-  simpl in |- *; simpl in H1; right; symmetry  in |- *; assumption.
+  simpl; simpl in H1; right; symmetry ; assumption.
   assert
     (H2 :
       In
@@ -557,7 +557,7 @@ Proof.
         (pos_Rl (cons_ORlist (cons r l1) l2)
           (pred (Rlength (cons_ORlist (cons r l1) l2)))));
       intros; apply H3; exists (pred (Rlength (cons_ORlist (cons r l1) l2)));
-        split; [ reflexivity | rewrite RList_P11; simpl in |- *; apply lt_n_Sn ]
+        split; [ reflexivity | rewrite RList_P11; simpl; apply lt_n_Sn ]
       | elim
         (RList_P9 (cons r l1) l2
           (pos_Rl (cons_ORlist (cons r l1) l2)
@@ -565,7 +565,7 @@ Proof.
         intros; assert (H5 := H3 H2); elim H5; intro;
           [ apply RList_P7; assumption | rewrite H1; apply RList_P7; assumption ] ].
   induction  l1 as [| r l1 Hrecl1].
-  simpl in |- *; simpl in H1; right; assumption.
+  simpl; simpl in H1; right; assumption.
   elim
     (RList_P9 (cons r l1) l2 (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
     intros;
@@ -573,10 +573,10 @@ Proof.
         (H4 :
           In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) (cons r l1) \/
           In (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))) l2);
-        [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1)) in |- *;
+        [ left; change (In (pos_Rl (cons r l1) (Rlength l1)) (cons r l1));
           elim (RList_P3 (cons r l1) (pos_Rl (cons r l1) (Rlength l1)));
             intros; apply H5; exists (Rlength l1); split;
-              [ reflexivity | simpl in |- *; apply lt_n_Sn ]
+              [ reflexivity | simpl; apply lt_n_Sn ]
           | assert (H5 := H3 H4); apply RList_P7;
             [ apply RList_P2; assumption
               | elim
@@ -587,7 +587,7 @@ Proof.
                     (RList_P3 (cons r l1)
                       (pos_Rl (cons r l1) (pred (Rlength (cons r l1)))));
                     intros; apply H9; exists (pred (Rlength (cons r l1)));
-                      split; [ reflexivity | simpl in |- *; apply lt_n_Sn ] ] ].
+                      split; [ reflexivity | simpl; apply lt_n_Sn ] ] ].
 Qed.
 
 Lemma RList_P17 :
@@ -599,14 +599,14 @@ Proof.
   simple induction l1.
   intros; elim H0.
   intros; induction  i as [| i Hreci].
-  simpl in |- *; elim H1; intro;
+  simpl; elim H1; intro;
     [ simpl in H2; rewrite H4 in H2; elim (Rlt_irrefl _ H2)
       | apply RList_P5; [ apply RList_P4 with r; assumption | assumption ] ].
-  simpl in |- *; simpl in H2; elim H1; intro.
+  simpl; simpl in H2; elim H1; intro.
   rewrite H4 in H2; assert (H5 : r <= pos_Rl r0 i);
     [ apply Rle_trans with (pos_Rl r0 0);
-      [ apply (H0 0%nat); simpl in |- *; simpl in H3; apply neq_O_lt;
-        red in |- *; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3)
+      [ apply (H0 0%nat); simpl; simpl in H3; apply neq_O_lt;
+        red; intro; rewrite <- H5 in H3; elim (lt_n_O _ H3)
         | elim (RList_P6 r0); intros; apply H5;
           [ apply RList_P4 with r; assumption
             | apply le_O_n
@@ -618,7 +618,7 @@ Proof.
       | simpl in H3; apply lt_S_n;
         replace (S (pred (Rlength r0))) with (Rlength r0);
         [ apply H3
-          | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
+          | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
             rewrite <- H5 in H3; elim (lt_n_O _ H3) ] ].
 Qed.
 
@@ -626,7 +626,7 @@ Lemma RList_P18 :
   forall (l:Rlist) (f:R -> R), Rlength (app_Rlist l f) = Rlength l.
 Proof.
   simple induction l; intros;
-    [ reflexivity | simpl in |- *; rewrite H; reflexivity ].
+    [ reflexivity | simpl; rewrite H; reflexivity ].
 Qed.
 
 Lemma RList_P19 :
@@ -666,7 +666,7 @@ Lemma RList_P23 :
     Rlength (cons_Rlist l1 l2) = (Rlength l1 + Rlength l2)%nat.
 Proof.
   simple induction l1;
-    [ intro; reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+    [ intro; reflexivity | intros; simpl; rewrite H; reflexivity ].
 Qed.
 
 Lemma RList_P24 :
@@ -685,9 +685,9 @@ Proof.
     [ replace (Rlength r0 + Rlength (cons r1 l2))%nat with
       (S (Rlength r0 + Rlength l2));
       [ reflexivity
-        | simpl in |- *; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
+        | simpl; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR;
           rewrite S_INR; ring ]
-      | simpl in |- *; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;
+      | simpl; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR;
         rewrite S_INR; ring ].
 Qed.
 
@@ -699,27 +699,27 @@ Lemma RList_P25 :
     ordered_Rlist (cons_Rlist l1 l2).
 Proof.
   simple induction l1.
-  intros; simpl in |- *; assumption.
+  intros; simpl; assumption.
   simple induction r0.
-  intros; simpl in |- *; simpl in H2; unfold ordered_Rlist in |- *; intros;
+  intros; simpl; simpl in H2; unfold ordered_Rlist; intros;
     simpl in H3.
   induction  i as [| i Hreci].
-  simpl in |- *; assumption.
-  change (pos_Rl l2 i <= pos_Rl l2 (S i)) in |- *; apply (H1 i); apply lt_S_n;
+  simpl; assumption.
+  change (pos_Rl l2 i <= pos_Rl l2 (S i)); apply (H1 i); apply lt_S_n;
     replace (S (pred (Rlength l2))) with (Rlength l2);
     [ assumption
-      | apply S_pred with 0%nat; apply neq_O_lt; red in |- *; intro;
+      | apply S_pred with 0%nat; apply neq_O_lt; red; intro;
         rewrite <- H4 in H3; elim (lt_n_O _ H3) ].
   intros; clear H; assert (H : ordered_Rlist (cons_Rlist (cons r1 r2) l2)).
   apply H0; try assumption.
   apply RList_P4 with r; assumption.
-  unfold ordered_Rlist in |- *; intros; simpl in H4;
+  unfold ordered_Rlist; intros; simpl in H4;
     induction  i as [| i Hreci].
-  simpl in |- *; apply (H1 0%nat); simpl in |- *; apply lt_O_Sn.
+  simpl; apply (H1 0%nat); simpl; apply lt_O_Sn.
   change
     (pos_Rl (cons_Rlist (cons r1 r2) l2) i <=
-      pos_Rl (cons_Rlist (cons r1 r2) l2) (S i)) in |- *;
-    apply (H i); simpl in |- *; apply lt_S_n; assumption.
+      pos_Rl (cons_Rlist (cons r1 r2) l2) (S i));
+    apply (H i); simpl; apply lt_S_n; assumption.
 Qed.
 
 Lemma RList_P26 :
@@ -738,13 +738,13 @@ Lemma RList_P27 :
     cons_Rlist l1 (cons_Rlist l2 l3) = cons_Rlist (cons_Rlist l1 l2) l3.
 Proof.
   simple induction l1; intros;
-    [ reflexivity | simpl in |- *; rewrite (H l2 l3); reflexivity ].
+    [ reflexivity | simpl; rewrite (H l2 l3); reflexivity ].
 Qed.
 
 Lemma RList_P28 : forall l:Rlist, cons_Rlist l nil = l.
 Proof.
   simple induction l;
-    [ reflexivity | intros; simpl in |- *; rewrite H; reflexivity ].
+    [ reflexivity | intros; simpl; rewrite H; reflexivity ].
 Qed.
 
 Lemma RList_P29 :
@@ -759,23 +759,23 @@ Proof.
     replace (cons_Rlist l1 (cons r r0)) with
     (cons_Rlist (cons_Rlist l1 (cons r nil)) r0).
   inversion H0.
-  rewrite <- minus_n_n; simpl in |- *; rewrite RList_P26.
+  rewrite <- minus_n_n; simpl; rewrite RList_P26.
   clear l2 r0 H i H0 H1 H2; induction  l1 as [| r0 l1 Hrecl1].
   reflexivity.
-  simpl in |- *; assumption.
-  rewrite RList_P23; rewrite plus_comm; simpl in |- *; apply lt_n_Sn.
+  simpl; assumption.
+  rewrite RList_P23; rewrite plus_comm; simpl; apply lt_n_Sn.
   replace (S m - Rlength l1)%nat with (S (S m - S (Rlength l1))).
-  rewrite H3; simpl in |- *;
+  rewrite H3; simpl;
     replace (S (Rlength l1)) with (Rlength (cons_Rlist l1 (cons r nil))).
   apply (H (cons_Rlist l1 (cons r nil)) i).
-  rewrite RList_P23; rewrite plus_comm; simpl in |- *; rewrite <- H3;
+  rewrite RList_P23; rewrite plus_comm; simpl; rewrite <- H3;
     apply le_n_S; assumption.
-  repeat rewrite RList_P23; simpl in |- *; rewrite RList_P23 in H1;
+  repeat rewrite RList_P23; simpl; rewrite RList_P23 in H1;
     rewrite plus_comm in H1; simpl in H1; rewrite (plus_comm (Rlength l1));
-      simpl in |- *; rewrite plus_comm; apply H1.
+      simpl; rewrite plus_comm; apply H1.
   rewrite RList_P23; rewrite plus_comm; reflexivity.
-  change (S (m - Rlength l1) = (S m - Rlength l1)%nat) in |- *;
+  change (S (m - Rlength l1) = (S m - Rlength l1)%nat);
     apply minus_Sn_m; assumption.
   replace (cons r r0) with (cons_Rlist (cons r nil) r0);
-  [ symmetry  in |- *; apply RList_P27 | reflexivity ].
+  [ symmetry ; apply RList_P27 | reflexivity ].
 Qed.
-- 
cgit v1.2.3