From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 theories/Logic/ClassicalDescription.v | 4 ++--
 theories/Logic/ClassicalFacts.v       | 6 ++----
 theories/Logic/ConstructiveEpsilon.v  | 4 ++--
 theories/Logic/Diaconescu.v           | 4 ++--
 4 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'theories/Logic')

diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 3737abf6..d15e2c96 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 10170 2007-10-03 14:41:25Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
 
 (** This file provides classical logic and definite description, which is
     equivalent to providing classical logic and Church's iota operator *)
@@ -21,7 +21,7 @@ Set Implicit Arguments.
 Require Export Classical.
 Require Import ChoiceFacts.
 
-Notation Local "'inhabited' A" := A (at level 200, only parsing).
+Notation Local inhabited A := A.
 
 Axiom constructive_definite_description :
   forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 734de52d..8a045ec8 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalFacts.v 10156 2007-09-30 19:02:14Z herbelin $ i*)
+(*i $Id: ClassicalFacts.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
 
 (** Some facts and definitions about classical logic
 
@@ -119,7 +119,7 @@ Qed.
 
 *)
 
-Definition inhabited (A:Prop) := A.
+Notation Local inhabited A := A.
 
 Lemma prop_ext_A_eq_A_imp_A :
   prop_extensionality -> forall A:Prop, inhabited A -> (A -> A) = A.
@@ -514,8 +514,6 @@ Qed.
     344 of Lecture Notes in Mathematics, Springer-Verlag, 1973.
 *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
-
 Definition IndependenceOfGeneralPremises :=
   forall (A:Type) (P:A -> Prop) (Q:Prop),
     inhabited A -> (Q -> exists x, P x) -> exists x, Q -> P x.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index f1503d24..3753b97b 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ConstructiveEpsilon.v 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
 
 (** This module proves the constructive description schema, which
 infers the sigma-existence (i.e., [Set]-existence) of a witness to a
@@ -53,7 +53,7 @@ of our searching algorithm. *)
 
 Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
-Notation Local "'acc' x" := (Acc R x) (at level 10).
+Notation Local acc x := (Acc R x).
 
 Lemma P_implies_acc : forall x : nat, P x -> acc x.
 Proof.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 5f139f35..880ef7e2 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Diaconescu.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Diaconescu.v 11238 2008-07-19 09:34:03Z herbelin $ i*)
 
 (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
    in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
@@ -267,7 +267,7 @@ End ProofIrrel_RelChoice_imp_EqEM.
 
 (** Proof sketch from Bell [Bell93] (with thanks to P. Castéran) *)
 
-Notation Local "'inhabited' A" := A (at level 10, only parsing).
+Notation Local inhabited A := A.
 
 Section ExtensionalEpsilon_imp_EM.
 
-- 
cgit v1.2.3