diff options
Diffstat (limited to 'theories/Bool')
| -rw-r--r-- | theories/Bool/Bool.v | 8 | ||||
| -rw-r--r-- | theories/Bool/BoolEq.v | 6 | ||||
| -rw-r--r-- | theories/Bool/Bvector.v | 4 | ||||
| -rw-r--r-- | theories/Bool/DecBool.v | 2 | ||||
| -rw-r--r-- | theories/Bool/IfProp.v | 2 | ||||
| -rw-r--r-- | theories/Bool/Sumbool.v | 2 | ||||
| -rw-r--r-- | theories/Bool/Zerob.v | 4 |
7 files changed, 14 insertions, 14 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index d5d11cea..a947e4fd 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.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 *) @@ -615,12 +615,12 @@ Proof. Qed. Hint Resolve absurd_eq_true. -(* A specific instance of trans_eq that preserves compatibility with +(* A specific instance of eq_trans that preserves compatibility with old hint bool_2 *) Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z. Proof. - apply trans_eq. + apply eq_trans. Qed. Hint Resolve trans_eq_bool. @@ -754,7 +754,7 @@ Notation "a &&& b" := (if a then b else false) Notation "a ||| b" := (if a then true else b) (at level 50, left associativity) : lazy_bool_scope. -Open Local Scope lazy_bool_scope. +Local Open Scope lazy_bool_scope. Lemma andb_lazy_alt : forall a b : bool, a && b = a &&& b. Proof. diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index d40e56bf..34777491 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.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 *) @@ -52,12 +52,12 @@ Section Bool_eq_dec. Definition not_eq_false_beq : forall x y:A, x <> y -> false = beq x y. Proof. intros x y H. - symmetry in |- *. + symmetry . apply not_true_is_false. intro. apply H. apply beq_eq. - symmetry in |- *. + symmetry . assumption. Defined. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 0c218163..d7162e62 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.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 *) @@ -13,7 +13,7 @@ Require Vector. Export Vector.VectorNotations. Require Import Minus. -Open Local Scope nat_scope. +Local Open Scope nat_scope. (** We build bit vectors in the spirit of List.v. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 3f03d2c1..ae01b9da 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.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 *) diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 6872eaea..57ffa6a4 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.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 *) diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 24b6a776..5a9daa94 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.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 *) diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index bac4c0d6..e8798d0d 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.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 *) @@ -9,7 +9,7 @@ Require Import Arith. Require Import Bool. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Definition zerob (n:nat) : bool := match n with |