Make standard library independent of the names generated by

induction/elim over a dependent elimination principle for Prop
arguments.

1 files changed, 6 insertions, 6 deletions

diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index d2c04f556..ef5d37bff 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -69,19 +69,19 @@ Proof.
         [ assumption | ring ] ].
   assert (H11 : (0 <= up x)%Z).
   apply le_IZR; apply Rle_trans with x; [ apply H6 | left; assumption ].
-  assert (H12 := IZN_var H11); elim H12; clear H12; intros; assert (H13 : E x).
+  assert (H12 := IZN_var H11); elim H12; clear H12; intros x0 H8; assert (H13 : E x).
   elim (classic (E x)); intro; try assumption.
   cut (forall y:R, E y -> y <= x - 1).
-  intro; assert (H14 := H5 _ H13); cut (x - 1 < x).
-  intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)).
+  intro H13; assert (H14 := H5 _ H13); cut (x - 1 < x).
+  intro H15; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H14 H15)).
   apply Rminus_lt; replace (x - 1 - x) with (-1); [ idtac | ring ];
     rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply Rlt_0_1.
-  intros; assert (H14 := H4 _ H13); elim H14; intro; unfold E in H13; elim H13;
-    intros; elim H16; intros; apply Rplus_le_reg_l with 1.
+  intros y H13; assert (H14 := H4 _ H13); elim H14; intro H15; unfold E in H13; elim H13;
+    intros x1 H16; elim H16; intros H17 H18; apply Rplus_le_reg_l with 1.
   replace (1 + (x - 1)) with x; [ idtac | ring ]; rewrite <- H18;
     replace (1 + INR x1) with (INR (S x1)); [ idtac | rewrite S_INR; ring ].
   cut (x = INR (pred x0)).
-  intro; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
+  intro H19; rewrite H19; apply le_INR; apply lt_le_S; apply INR_lt; rewrite H18;
     rewrite <- H19; assumption.
   rewrite H10; rewrite H8; rewrite <- INR_IZR_INZ; replace 1 with (INR 1);
     [ idtac | reflexivity ]; rewrite <- minus_INR.