From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/Bool/Bool.v    | 8 ++++----
 theories/Bool/BoolEq.v  | 6 +++---
 theories/Bool/Bvector.v | 4 ++--
 theories/Bool/DecBool.v | 2 +-
 theories/Bool/IfProp.v  | 2 +-
 theories/Bool/Sumbool.v | 2 +-
 theories/Bool/Zerob.v   | 4 ++--
 7 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'theories/Bool')

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
-- 
cgit v1.2.3