diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /lib/Ordered.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip | |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'lib/Ordered.v')
| -rw-r--r-- | lib/Ordered.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/lib/Ordered.v b/lib/Ordered.v index a2c36673..c333cc50 100644 --- a/lib/Ordered.v +++ b/lib/Ordered.v @@ -31,11 +31,11 @@ Definition eq (x y: t) := x = y. Definition lt := Plt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof Plt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. @@ -58,16 +58,16 @@ Module OrderedZ <: OrderedType. Definition t := Z. Definition eq (x y: t) := x = y. -Definition lt := Zlt. +Definition lt := Z.lt. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. -Proof Zlt_trans. +Proof Z.lt_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. unfold lt, eq, t; intros. omega. Qed. Lemma compare : forall x y : t, Compare lt eq x y. @@ -91,11 +91,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Int.unsigned x < Int.unsigned y. Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. unfold lt; intros. omega. @@ -129,11 +129,11 @@ Definition eq (x y: t) := x = y. Definition lt (x y: t) := Plt (A.index x) (A.index y). Lemma eq_refl : forall x : t, eq x x. -Proof (@refl_equal t). +Proof (@eq_refl t). Lemma eq_sym : forall x y : t, eq x y -> eq y x. -Proof (@sym_equal t). +Proof (@eq_sym t). Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z. -Proof (@trans_equal t). +Proof (@eq_trans t). Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z. Proof. |