diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-24 17:28:51 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-24 17:28:51 +0200 |
commit | 7e38b6627caaab7d19c4fc0ee542a67d9f8970c2 (patch) | |
tree | 375ed6a0a45131e479dea6d3d8c9cf64a786fcf7 /theories/Reals/RIneq.v | |
parent | 46462c3cc69e97bf3260f1aad5faaa6eaf6c2722 (diff) |
Remove v62 from stdlib.
This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.
Diffstat (limited to 'theories/Reals/RIneq.v')
-rw-r--r-- | theories/Reals/RIneq.v | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index f26bac2bb..379fee6f4 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -389,7 +389,7 @@ Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. Proof. split; ring. Qed. -Hint Resolve Rplus_ne: real v62. +Hint Resolve Rplus_ne: real. (**********) @@ -425,7 +425,6 @@ Proof. apply (f_equal (fun v => v + r)). Qed. -(*i Old i*)Hint Resolve Rplus_eq_compat_l: v62. (**********) Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 = r + r2 -> r1 = r2. @@ -501,21 +500,21 @@ Lemma Rmult_0_r : forall r, r * 0 = 0. Proof. intro; ring. Qed. -Hint Resolve Rmult_0_r: real v62. +Hint Resolve Rmult_0_r: real. (**********) Lemma Rmult_0_l : forall r, 0 * r = 0. Proof. intro; ring. Qed. -Hint Resolve Rmult_0_l: real v62. +Hint Resolve Rmult_0_l: real. (**********) Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r. Proof. intro; split; ring. Qed. -Hint Resolve Rmult_ne: real v62. +Hint Resolve Rmult_ne: real. (**********) Lemma Rmult_1_r : forall r, r * 1 = r. @@ -530,7 +529,6 @@ Proof. auto with real. Qed. -(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62. Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r. Proof. @@ -646,7 +644,7 @@ Lemma Ropp_0 : -0 = 0. Proof. ring. Qed. -Hint Resolve Ropp_0: real v62. +Hint Resolve Ropp_0: real. (**********) Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0. |