diff options
Diffstat (limited to 'theories/Arith/Compare_dec.v')
| -rw-r--r-- | theories/Arith/Compare_dec.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 360d760a..a90a9ce9 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -11,7 +11,7 @@ Require Import Lt. Require Import Gt. Require Import Decidable. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Implicit Types m n x y : nat. @@ -138,7 +138,7 @@ Proof. Qed. -(** A ternary comparison function in the spirit of [Zcompare]. *) +(** A ternary comparison function in the spirit of [Z.compare]. *) Fixpoint nat_compare n m := match n, m with @@ -202,7 +202,7 @@ Lemma nat_compare_spec : forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). Proof. intros. - destruct (nat_compare x y) as [ ]_eqn; constructor. + destruct (nat_compare x y) eqn:?; constructor. apply nat_compare_eq; auto. apply <- nat_compare_lt; auto. apply <- nat_compare_gt; auto. @@ -256,7 +256,7 @@ Lemma leb_correct : forall m n, m <= n -> leb m n = true. Proof. induction m as [| m IHm]. trivial. destruct n. intro H. elim (le_Sn_O _ H). - intros. simpl in |- *. apply IHm. apply le_S_n. assumption. + intros. simpl. apply IHm. apply le_S_n. assumption. Qed. Lemma leb_complete : forall m n, leb m n = true -> m <= n. |