aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-26 14:23:06 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-06-26 14:50:12 +0200
commit55e46598fac67157a5b2c820be621d254581b888 (patch)
tree61db2f9a76b3bb55c5fc0131be9600227efc31c2 /theories
parent68d60b7c33b11ad452eca3d2a7ec320963064a9d (diff)
Deactivate the "Standard Propositions Naming" flag, source of a lot of
incompatibilities, at least until the check of compilation of contribs succeeds more often. Incidentally adapted some proofs in Reals which were not agnostic relatively to whether the option is on or off.
Diffstat (limited to 'theories')
-rw-r--r--theories/Reals/Alembert.v12
-rw-r--r--theories/Reals/SeqSeries.v4
2 files changed, 8 insertions, 8 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index c4416e5d8..c037fdd20 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -472,11 +472,11 @@ Proof.
elim Hyp; intros; assumption.
elim H3; intros; assumption.
apply Rminus_eq_contra.
- red; intro.
- elim H3; intros.
+ red; intro H10.
+ elim H3; intros H11 H12.
rewrite H10 in H12; elim (Rlt_irrefl _ H12).
- red; intro.
- elim H3; intros.
+ red; intro H10.
+ elim H3; intros H11 H12.
rewrite H10 in H12; elim (Rlt_irrefl _ H12).
replace (An (S x0)) with (An (S x0 + 0)%nat).
apply (tech6 (fun i:nat => An (S x0 + i)%nat) x).
@@ -485,7 +485,7 @@ Proof.
elim H3; intros; assumption.
intro.
cut (forall n:nat, (n >= x0)%nat -> An (S n) < x * An n).
- intro.
+ intro H9.
replace (S x0 + S i)%nat with (S (S x0 + i)).
apply H9.
unfold ge.
@@ -507,7 +507,7 @@ Proof.
apply Rmult_lt_0_compat.
apply H.
apply Rinv_0_lt_compat; apply H.
- red; intro.
+ red; intro H10.
assert (H11 := H n).
rewrite H10 in H11; elim (Rlt_irrefl _ H11).
replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ].
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index fb0c171ad..fc143ce71 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -229,7 +229,7 @@ Proof.
do 2 rewrite <- Rplus_assoc; do 2 rewrite Rplus_opp_r;
do 2 rewrite Rplus_0_l; do 2 rewrite Rabs_Ropp; repeat rewrite Rabs_right.
apply sum_Rle; intros.
- elim (H (S n + n0)%nat); intros.
+ elim (H (S n + n0)%nat); intros H7 H8.
apply H8.
apply Rle_ge; apply cond_pos_sum; intro.
elim (H (S n + n0)%nat); intros.
@@ -246,7 +246,7 @@ Proof.
do 2 rewrite Rplus_assoc; do 2 rewrite Rplus_opp_l;
do 2 rewrite Rplus_0_r; repeat rewrite Rabs_right.
apply sum_Rle; intros.
- elim (H (S m + n0)%nat); intros; apply H8.
+ elim (H (S m + n0)%nat); intros H7 H8; apply H8.
apply Rle_ge; apply cond_pos_sum; intro.
elim (H (S m + n0)%nat); intros.
apply Rle_trans with (An (S m + n0)%nat); assumption.