Clear sur hypothese non definie

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

2 files changed, 2 insertions, 2 deletions

diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 9dbd9cbc36..809c5de6d4 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -347,7 +347,7 @@ Rewrite S_INR; Ring.
 Assumption.
 Apply le_lt_n_Sm; Assumption.
 Apply Rge_minus; Apply Rle_sym1; Assumption.
-Intros; Clear H0 eos H1 H4 phi H5 H6 t H7; Case (Req_EM t0 b); Intro.
+Intros; Clear H0 H1 H4 phi H5 H6 t H7; Case (Req_EM t0 b); Intro.
 Left; Assumption.
 Right; Pose I := [j:nat]``a+(INR j)*del<=t0``; Assert H1 : (EX n:nat | (I n)).
 Exists O; Unfold I; Rewrite Rmult_Ol; Rewrite Rplus_Or; Elim H8; Intros; Assumption.
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index fd75ae4d84..a6c1c7a08e 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -920,7 +920,7 @@ Pose g' := [x:R]Cases (total_order_Rle r1 x) of
 Assert H7 : ``r1<=b``.
 Rewrite <- H4; Apply RList_P7; [Assumption | Left; Reflexivity].
 Assert H8 : (IsStepFun g' a b).
-Unfold IsStepFun; Assert H8 := (pre g); Unfold IsStepFun in H8; Elim H8; Intros lg H9; Unfold is_subdivision in H9; Elim H9; Clear H9 H10; Intros lg2 H9; Split with (cons a lg); Unfold is_subdivision; Split with (cons (f a) lg2); Unfold adapted_couple in H9; Decompose [and] H9; Clear H9; Unfold adapted_couple; Repeat Split.
+Unfold IsStepFun; Assert H8 := (pre g); Unfold IsStepFun in H8; Elim H8; Intros lg H9; Unfold is_subdivision in H9; Elim H9; Clear H9; Intros lg2 H9; Split with (cons a lg); Unfold is_subdivision; Split with (cons (f a) lg2); Unfold adapted_couple in H9; Decompose [and] H9; Clear H9; Unfold adapted_couple; Repeat Split.
 Unfold ordered_Rlist; Intros; Simpl in H9; Induction i.
 Simpl; Rewrite H12; Replace (Rmin r1 b) with r1.
 Simpl in H0; Rewrite <- H0; Apply (H O); Simpl; Apply lt_O_Sn.