diff options
| -rw-r--r-- | theories/Structures/OrdersFacts.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index d5a76ee69f..4ac54d280a 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -102,10 +102,10 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull'). Proof. iorder. Qed. Lemma le_or_gt : forall x y, x<=y \/ y<x. - Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. + Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed. Lemma lt_or_ge : forall x y, x<y \/ y<=x. - Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed. + Proof. intros x y. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed. Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x. Proof. iorder. Qed. @@ -175,11 +175,11 @@ Module OrderedTypeFacts (Import O: OrderedType'). Definition eqb x y : bool := if eq_dec x y then true else false. - Lemma if_eq_dec : forall x y (B:Type)(b b':B), + Lemma if_eq_dec x y (B:Type)(b b':B) : (if eq_dec x y then b else b') = (match compare x y with Eq => b | _ => b' end). Proof. - intros; destruct eq_dec; elim_compare x y; auto; order. + destruct eq_dec; elim_compare x y; auto; order. Qed. Lemma eqb_alt : @@ -257,7 +257,7 @@ Definition compare := flip O.compare. Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y). Proof. -intros; unfold compare, eq, lt, flip. +intros x y; unfold compare, eq, lt, flip. destruct (O.compare_spec y x); auto with relations. Qed. |