diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 16:56:37 +0000 |
| commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
| tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /theories/Reals/Rlogic.v | |
| parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) | |
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
Diffstat (limited to 'theories/Reals/Rlogic.v')
| -rw-r--r-- | theories/Reals/Rlogic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 2237ea6ef..5cb0a2ffb 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -271,10 +271,10 @@ assert (H2 : ~ is_upper_bound E M'). intro H5. assert (M <= M')%R by (apply H4; exact H5). apply (Rlt_not_le M M'). - unfold M' in |- *. - pattern M at 2 in |- *. + unfold M'. + pattern M at 2. rewrite <- Rplus_0_l. - pattern (0 + M)%R in |- *. + pattern (0 + M)%R. rewrite Rplus_comm. rewrite <- (Rplus_opp_r 1). apply Rplus_lt_compat_l. @@ -284,7 +284,7 @@ assert (H2 : ~ is_upper_bound E M'). apply H2. intros N (n,H7). rewrite H7. -unfold M' in |- *. +unfold M'. assert (H5 : (INR (S n) <= M)%R) by (apply H3; exists (S n); reflexivity). rewrite S_INR in H5. assert (H6 : (INR n + 1 + -1 <= M + -1)%R). |