Imported Upstream version 8.4~betaupstream/8.4_beta

29 files changed, 343 insertions, 129 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index d954f40c..2b388687 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Berardi.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file formalizes Berardi's paradox which says that in
    the calculus of constructions, excluded middle (EM) and axiom of
    choice (AC) imply proof irrelevance (PI).
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 60dbf3ea..8d82bc8e 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -1,14 +1,12 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ChoiceFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Some facts and definitions concerning choice and description in
        intuitionistic logic.
 
diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index 3f36ff38..9362a11f 100644
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* File created for Coq V5.10.14b, Oct 1995 *)
 
 (** Classical Logic *)
 
diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v
index 17b08a2f..6bc0be1d 100644
--- a/theories/Logic/ClassicalChoice.v
+++ b/theories/Logic/ClassicalChoice.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides classical logic and functional choice; this
     especially provides both indefinite descriptions and choice functions
     but this is weaker than providing epsilon operator and classical logic
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index ad454a4d..d35ed138 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalDescription.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides classical logic and definite description, which is
     equivalent to providing classical logic and Church's iota operator *)
 
@@ -18,14 +16,12 @@
 
 Set Implicit Arguments.
 
-Require Export Classical.
+Require Export Classical.   (* Axiomatize classical reasoning *)
+Require Export Description. (* Axiomatize constructive form of Church's iota *)
 Require Import ChoiceFacts.
 
 Notation Local inhabited A := A (only parsing).
 
-Axiom constructive_definite_description :
-  forall (A : Type) (P : A->Prop), (exists! x : A, P x) -> { x : A | P x }.
-
 (** The idea for the following proof comes from [ChicliPottierSimpson02] *)
 
 Theorem excluded_middle_informative : forall P:Prop, {P} + {~ P}.
diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v
index 52ecadaf..ae32b127 100644
--- a/theories/Logic/ClassicalEpsilon.v
+++ b/theories/Logic/ClassicalEpsilon.v
@@ -1,14 +1,12 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides classical logic and indefinite description under
     the form of Hilbert's epsilon operator *)
 
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 5f4516dd..bcec657a 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -1,14 +1,12 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Some facts and definitions about classical logic
 
 Table of contents:
diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v
index fafa0b94..ebb73b19 100644
--- a/theories/Logic/ClassicalUniqueChoice.v
+++ b/theories/Logic/ClassicalUniqueChoice.v
@@ -1,14 +1,12 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ClassicalUniqueChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides classical logic and unique choice; this is
     weaker than providing iota operator and classical logic as the
     definite descriptions provided by the axiom of unique choice can
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index 06502d63..7d8bde71 100644
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -1,12 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical_Pred_Set.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* File created for Coq V5.10.14b, Oct 1995, by duplication of
+   Classical_Pred_Type.v *)
 
 (** This file is obsolete, use Classical_Pred_Type.v via Classical.v
 instead *)
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index bcd529f0..9d57fe88 100644
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -1,12 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical_Pred_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* This file is a renaming for V5.10.14b, Oct 1995, of file Classical.v
+   introduced in Coq V5.8.3, June 1993 *)
 
 (** Classical Predicate Logic on Type *)
 
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index c51050d5..d2b35da2 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -1,12 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical_Prop.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* File created for Coq V5.10.14b, Oct 1995 *)
+(* Classical tactics for proving disjunctions by Julien Narboux, Jul 2005 *)
+(* Inferred proof-irrelevance and eq_rect_eq added by Hugo Herbelin, Mar 2006 *)
 
 (** Classical Propositional Logic *)
 
diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v
index 94e623bd..9b28a6ab 100644
--- a/theories/Logic/Classical_Type.v
+++ b/theories/Logic/Classical_Type.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Classical_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file is obsolete, use Classical.v instead *)
 
 (** Classical Logic for Type *)
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
index 004fdef3..33550389 100644
--- a/theories/Logic/ConstructiveEpsilon.v
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -1,26 +1,25 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ConstructiveEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(*i $Id: ConstructiveEpsilon.v 14628 2011-11-03 23:22:45Z herbelin $ i*)
 
-(*i $Id: ConstructiveEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(** This module proves the constructive description schema, which
-infers the sigma-existence (i.e., [Set]-existence) of a witness to a
-predicate from the regular existence (i.e., [Prop]-existence). One
-requires that the underlying set is countable and that the predicate
-is decidable. *)
+(** This provides with a proof of the constructive form of definite
+and indefinite descriptions for Sigma^0_1-formulas (hereafter called
+"small" formulas), which infers the sigma-existence (i.e.,
+[Type]-existence) of a witness to a decidable predicate over a
+countable domain from the regular existence (i.e.,
+[Prop]-existence). *)
 
 (** Coq does not allow case analysis on sort [Prop] when the goal is in
-[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
+not in [Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
 show [{n : nat | P n}]. However, one can perform a recursion on an
 inductive predicate in sort [Prop] so that the returning type of the
-recursion is in [Set]. This trick is described in Coq'Art book, Sect.
+recursion is in [Type]. This trick is described in Coq'Art book, Sect.
 14.2.3 and 15.4. In particular, this trick is used in the proof of
 [Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
 inductive predicate [Acc] and the resulting type is in [Type].
@@ -41,7 +40,7 @@ For the first one we provide explicit and short proof terms. *)
 
 (* Direct version *)
 
-Section ConstructiveIndefiniteDescription_Direct.
+Section ConstructiveIndefiniteGroundDescription_Direct.
 
 Variable P : nat -> Prop.
 
@@ -79,11 +78,11 @@ Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} :=
     | right no => linear_search (S m) (inv_before_witness m b no)
   end.
 
-Definition constructive_indefinite_description_nat :
+Definition constructive_indefinite_ground_description_nat :
   (exists n, P n) -> {n:nat | P n} :=
   fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)).
 
-End ConstructiveIndefiniteDescription_Direct.
+End ConstructiveIndefiniteGroundDescription_Direct.
 
 (************************************************************************)
 
@@ -91,7 +90,7 @@ End ConstructiveIndefiniteDescription_Direct.
 
 Require Import Arith.
 
-Section ConstructiveIndefiniteDescription_Acc.
+Section ConstructiveIndefiniteGroundDescription_Acc.
 
 Variable P : nat -> Prop.
 
@@ -151,40 +150,40 @@ destruct (IH y Ryx) as [n Hn].
 exists n; assumption.
 Defined.
 
-Theorem constructive_indefinite_description_nat_Acc :
+Theorem constructive_indefinite_ground_description_nat_Acc :
   (exists n : nat, P n) -> {n : nat | P n}.
 Proof.
 intros H; apply acc_implies_P_eventually.
 apply P_eventually_implies_acc_ex; assumption.
 Defined.
 
-End ConstructiveIndefiniteDescription_Acc.
+End ConstructiveIndefiniteGroundDescription_Acc.
 
 (************************************************************************)
 
-Section ConstructiveEpsilon_nat.
+Section ConstructiveGroundEpsilon_nat.
 
 Variable P : nat -> Prop.
 
 Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
 
-Definition constructive_epsilon_nat (E : exists n : nat, P n) : nat
-  := proj1_sig (constructive_indefinite_description_nat P P_decidable E).
+Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat
+  := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E).
 
-Definition constructive_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_epsilon_nat E)
-  := proj2_sig (constructive_indefinite_description_nat P P_decidable E).
+Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E)
+  := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E).
 
-End ConstructiveEpsilon_nat.
+End ConstructiveGroundEpsilon_nat.
 
 (************************************************************************)
 
-Section ConstructiveEpsilon.
+Section ConstructiveGroundEpsilon.
 
 (** For the current purpose, we say that a set [A] is countable if
 there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
 a left inverse of [f]. *)
 
-Variable A : Set.
+Variable A : Type.
 Variable f : A -> nat.
 Variable g : nat -> A.
 
@@ -201,24 +200,43 @@ Proof.
 intro n; unfold P'; destruct (P_decidable (g n)); auto.
 Defined.
 
-Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
+Lemma constructive_indefinite_ground_description : (exists x : A, P x) -> {x : A | P x}.
 Proof.
 intro H. assert (H1 : exists n : nat, P' n).
 destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
-apply (constructive_indefinite_description_nat P' P'_decidable)  in H1.
+apply (constructive_indefinite_ground_description_nat P' P'_decidable)  in H1.
 destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
 Defined.
 
-Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
+Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}.
 Proof.
-  intros; apply constructive_indefinite_description; firstorder.
+  intros; apply constructive_indefinite_ground_description; firstorder.
 Defined.
 
-Definition constructive_epsilon (E : exists x : A, P x) : A
-  := proj1_sig (constructive_indefinite_description E).
-
-Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E)
-  := proj2_sig (constructive_indefinite_description E).
-
-End ConstructiveEpsilon.
-
+Definition constructive_ground_epsilon (E : exists x : A, P x) : A
+  := proj1_sig (constructive_indefinite_ground_description E).
+
+Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E)
+  := proj2_sig (constructive_indefinite_ground_description E).
+
+End ConstructiveGroundEpsilon.
+
+(* begin hide *)
+(* Compatibility: the qualificative "ground" was absent from the initial
+names of the results in this file but this had introduced confusion
+with the similarly named statement in Description.v *)
+Notation constructive_indefinite_description_nat :=
+  constructive_indefinite_ground_description_nat (only parsing).
+Notation constructive_epsilon_spec_nat :=
+  constructive_ground_epsilon_spec_nat (only parsing).
+Notation constructive_epsilon_nat :=
+  constructive_ground_epsilon_nat (only parsing).
+Notation constructive_indefinite_description :=
+  constructive_indefinite_ground_description (only parsing).
+Notation constructive_definite_description :=
+  constructive_definite_ground_description (only parsing).
+Notation constructive_epsilon_spec :=
+  constructive_ground_epsilon_spec (only parsing).
+Notation constructive_epsilon :=
+  constructive_ground_epsilon (only parsing).
+(* end hide *)
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index ace50884..fec7904e 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i 	$Id: Decidable.v 14641 2011-11-06 11:59:10Z herbelin $	 i*)
-
 (** Properties of decidable propositions *)
 
 Definition decidable (P:Prop) := P \/ ~ P.
diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v
index c59d8460..b74ebcc8 100644
--- a/theories/Logic/Description.v
+++ b/theories/Logic/Description.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Description.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides a constructive form of definite description; it
     allows to build functions from the proof of their existence in any
     context; this is weaker than Church's iota operator *)
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index 257245cc..8569e55e 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -1,14 +1,12 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Diaconescu.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle
    in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show
    that the axiom of choice in equivalence classes entails
@@ -158,8 +156,8 @@ End PredExt_RelChoice_imp_EM.
 (**********************************************************************)
 (** * B. Proof-Irrel. + Rel. Axiom of Choice -> Excl.-Middle for Equality *)
 
-(** This is an adaptation of Diaconescu's paradox exploiting that
-    proof-irrelevance is some form of extensionality *)
+(** This is an adaptation of Diaconescu's theorem, exploiting the
+    form of extensionality provided by proof-irrelevance *)
 
 Section ProofIrrel_RelChoice_imp_EqEM.
 
diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v
index 9134b3aa..cb8f8a73 100644
--- a/theories/Logic/Epsilon.v
+++ b/theories/Logic/Epsilon.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Epsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides indefinite description under the form of
     Hilbert's epsilon operator; it does not assume classical logic. *)
 
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 7918061c..b8e99036 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -1,13 +1,15 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Eqdep.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *)
+(* Abstraction with respect to the eq_rect_eq axiom and creation of
+   EqdepFacts.v by Hugo Herbelin, Mar 2006 *)
 
 (** This file axiomatizes the invariance by substitution of reflexive
     equality proofs [[Streicher93]] and exports its consequences, such
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 2d5f1537..d84cd824 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -1,13 +1,17 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: EqdepFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *)
+(* Further documentation and variants of eq_rect_eq by Hugo Herbelin,
+   Apr 2003 *)
+(* Abstraction with respect to the eq_rect_eq axiom and renaming to
+   EqdepFacts.v by Hugo Herbelin, Mar 2006 *)
 
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
@@ -33,7 +37,8 @@
 
 Table of contents:
 
-1. Definition of dependent equality and equivalence with equality
+1. Definition of dependent equality and equivalence with equality of
+   dependent pairs and with dependent pair of equalities
 
 2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
 
@@ -45,6 +50,8 @@ Table of contents:
 (************************************************************************)
 (** * Definition of dependent equality and equivalence with equality of dependent pairs *)
 
+Import EqNotations.
+
 Section Dependent_Equality.
 
   Variable U : Type.
@@ -75,11 +82,11 @@ Section Dependent_Equality.
 
   Scheme eq_indd := Induction for eq Sort Prop.
 
-  (** Equivalent definition of dependent equality expressed as a non
-      dependent inductive type *)
+  (** Equivalent definition of dependent equality as a dependent pair of
+      equalities *)
 
   Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
-    eq_dep1_intro : forall h:q = p, x = eq_rect q P y p h -> eq_dep1 p x q y.
+    eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y.
 
   Lemma eq_dep1_dep :
     forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.
@@ -95,13 +102,13 @@ Section Dependent_Equality.
   Proof.
     destruct 1.
     apply eq_dep1_intro with (refl_equal p).
-    simpl in |- *; trivial.
+    simpl; trivial.
   Qed.
 
 End Dependent_Equality.
 
-Implicit Arguments eq_dep [U P].
-Implicit Arguments eq_dep1 [U P].
+Arguments eq_dep  [U P] p x q _.
+Arguments eq_dep1 [U P] p x q y.
 
 (** Dependent equality is equivalent to equality on dependent pairs *)
 
@@ -116,24 +123,103 @@ Qed.
 
 Notation eq_sigS_eq_dep := eq_sigT_eq_dep (only parsing). (* Compatibility *)
 
-Lemma equiv_eqex_eqdep :
+Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-   existT P p x = existT P q y <-> eq_dep p x q y.
+    eq_dep p x q y -> existT P p x = existT P q y.
 Proof.
-  split.
-  (* -> *)
-  apply eq_sigT_eq_dep.
-  (* <- *)
   destruct 1; reflexivity.
 Qed.
 
-Lemma eq_dep_eq_sigT :
+Lemma eq_sigT_iff_eq_dep :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
-    eq_dep p x q y -> existT P p x = existT P q y.
+    existT P p x = existT P q y <-> eq_dep p x q y.
+Proof.
+  split; auto using eq_sigT_eq_dep, eq_dep_eq_sigT.
+Qed.
+
+Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *)
+
+Lemma eq_sig_eq_dep :
+  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+    exist P p x = exist P q y -> eq_dep p x q y.
+Proof.
+  intros.
+  dependent rewrite H.
+  apply eq_dep_intro.
+Qed.
+
+Lemma eq_dep_eq_sig :
+  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+    eq_dep p x q y -> exist P p x = exist P q y.
 Proof.
   destruct 1; reflexivity.
 Qed.
 
+Lemma eq_sig_iff_eq_dep :
+  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
+    exist P p x = exist P q y <-> eq_dep p x q y.
+Proof.
+  split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
+Qed.
+
+(** Dependent equality is equivalent to a dependent pair of equalities *)
+
+Set Implicit Arguments.
+
+Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.
+Proof.
+  intros; split; intro H.
+  - change x2 with (projT1 (existT P x2 H2)).
+    change H2 with (projT2 (existT P x2 H2)) at 5.
+    destruct H. simpl.
+    exists eq_refl.
+    reflexivity.
+  - destruct H as (->,<-).
+    reflexivity.
+Defined.
+
+Lemma eq_sigT_fst :
+  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2.
+Proof.
+  intros.
+  change x2 with (projT1 (existT P x2 H2)).
+  destruct H.
+  reflexivity.
+Defined.
+
+Lemma eq_sigT_snd :
+  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2.
+Proof.
+  intros.
+  unfold eq_sigT_fst.
+  change x2 with (projT1 (existT P x2 H2)).
+  change H2 with (projT2 (existT P x2 H2)) at 3.
+  destruct H.
+  reflexivity.
+Defined.
+
+Lemma eq_sig_fst :
+  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2.
+Proof.
+  intros.
+  change x2 with (proj1_sig (exist P x2 H2)).
+  destruct H.
+  reflexivity.
+Defined.
+
+Lemma eq_sig_snd :
+  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2.
+Proof.
+  intros.
+  unfold eq_sig_fst, eq_ind.
+  change x2 with (proj1_sig (exist P x2 H2)).
+  change H2 with (proj2_sig (exist P x2 H2)) at 3.
+  destruct H.
+  reflexivity.
+Defined.
+
+Unset Implicit Arguments.
+
 (** Exported hints *)
 
 Hint Resolve eq_dep_intro: core.
@@ -326,5 +412,5 @@ Notation inj_pairT2 := inj_pair2.
 
 End EqdepTheory.
 
-Implicit Arguments eq_dep [].
-Implicit Arguments eq_dep1 [].
+Arguments eq_dep  U P p x q _ : clear implicits.
+Arguments eq_dep1 U P p x q y : clear implicits.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 77908b08..59088aa7 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -1,12 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Eqdep_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Bruno Barras, Jan 1998 *)
+(* Made a module instance for EqdepFacts by Hugo Herbelin, Mar 2006 *)
 
 (** We prove that there is only one proof of [x=x], i.e [refl_equal x].
     This holds if the equality upon the set of [x] is decidable.
diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v
new file mode 100644
index 00000000..f5e71ef4
--- /dev/null
+++ b/theories/Logic/ExtensionalityFacts.v
@@ -0,0 +1,136 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Some facts and definitions about extensionality
+
+We investigate the relations between the following extensionality principles
+
+- Functional extensionality
+- Equality of projections from diagonal
+- Unicity of inverse bijections
+- Bijectivity of bijective composition
+
+Table of contents
+
+1. Definitions
+
+2. Functional extensionality <-> Equality of projections from diagonal
+
+3. Functional extensionality <-> Unicity of inverse bijections
+
+4. Functional extensionality <-> Bijectivity of bijective composition
+
+*)
+
+Set Implicit Arguments.
+
+(**********************************************************************)
+(** * Definitions *)
+
+(** Being an inverse *)
+
+Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g b) = b).
+
+(** The diagonal over A and the one-one correspondence with A *)
+
+Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }.
+
+Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}.
+
+Arguments pi1 {A} _.
+Arguments pi2 {A} _.
+
+Lemma diagonal_projs_same_behavior : forall A (x:Delta A), pi1 x = pi2 x.
+Proof.
+  destruct x as (a1,a2,Heq); assumption.
+Qed.
+
+Lemma diagonal_inverse1 : forall A, is_inverse (A:=A) delta pi1.
+Proof.
+  split; [trivial|]; destruct b as (a1,a2,[]); reflexivity.
+Qed.
+
+Lemma diagonal_inverse2 : forall A, is_inverse (A:=A) delta pi2.
+Proof.
+  split; [trivial|]; destruct b as (a1,a2,[]); reflexivity.
+Qed.
+
+(** Functional extensionality *)
+
+Local Notation FunctionalExtensionality := 
+  (forall A B (f g : A -> B), (forall x, f x = g x) -> f = g).
+
+(** Equality of projections from diagonal *)
+
+Local Notation EqDeltaProjs := (forall A, pi1 = pi2 :> (Delta A -> A)).
+
+(** Unicity of bijection inverse *)
+
+Local Notation UniqueInverse := (forall A B (f:A->B) g1 g2, is_inverse f g1 -> is_inverse f g2 -> g1 = g2).
+
+(** Bijectivity of bijective composition *)
+
+Definition action A B C (f:A->B) := (fun h:B->C => fun x => h (f x)).
+
+Local Notation BijectivityBijectiveComp := (forall A B C (f:A->B) g,
+  is_inverse f g -> is_inverse (A:=B->C) (action f) (action g)).
+
+(**********************************************************************)
+(** * Functional extensionality <-> Equality of projections from diagonal *)
+
+Theorem FunctExt_iff_EqDeltaProjs : FunctionalExtensionality <-> EqDeltaProjs.
+Proof.
+  split.
+  - intros FunExt *; apply FunExt, diagonal_projs_same_behavior. 
+  - intros EqProjs **; change f with (fun x => pi1 {|pi1:=f x; pi2:=g x; eq:=H x|}).
+    rewrite EqProjs; reflexivity.
+Qed.
+
+(**********************************************************************)
+(** * Functional extensionality <-> Unicity of bijection inverse *)
+
+Lemma FunctExt_UniqInverse : FunctionalExtensionality -> UniqueInverse.
+Proof.
+  intros FunExt * (Hg1f,Hfg1) (Hg2f,Hfg2).
+  apply FunExt. intros; congruence.
+Qed.
+
+Lemma UniqInverse_EqDeltaProjs : UniqueInverse -> EqDeltaProjs.
+Proof.
+  intros UniqInv *.
+  apply UniqInv with delta; [apply diagonal_inverse1 | apply diagonal_inverse2].
+Qed.
+
+Theorem FunctExt_iff_UniqInverse : FunctionalExtensionality <-> UniqueInverse.
+Proof.
+  split. 
+  - apply FunctExt_UniqInverse.
+  - intro; apply FunctExt_iff_EqDeltaProjs, UniqInverse_EqDeltaProjs; trivial.
+Qed.
+
+(**********************************************************************)
+(** * Functional extensionality <-> Bijectivity of bijective composition *)
+
+Lemma FunctExt_BijComp : FunctionalExtensionality -> BijectivityBijectiveComp.
+Proof.
+  intros FunExt * (Hgf,Hfg). split; unfold action.
+  - intros h; apply FunExt; intro b; rewrite Hfg; reflexivity.
+  - intros h; apply FunExt; intro a; rewrite Hgf; reflexivity.
+Qed.
+
+Lemma BijComp_FunctExt : BijectivityBijectiveComp -> FunctionalExtensionality.
+Proof.
+  intros BijComp.
+  apply FunctExt_iff_UniqInverse. intros * H1 H2.
+  destruct BijComp with (C:=A) (1:=H2) as (Hg2f,_).
+  destruct BijComp with (C:=A) (1:=H1) as (_,Hfg1).
+  rewrite <- (Hg2f g1).
+  change g1 with (action g1 (fun x => x)).
+  rewrite -> (Hfg1 (fun x => x)).
+  reflexivity.
+Qed.
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index a696b6c8..35db160f 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: FunctionalExtensionality.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion.
    It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *)
 
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index afaeb51a..bb03c666 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v
index afca2ee1..8badc07c 100644
--- a/theories/Logic/IndefiniteDescription.v
+++ b/theories/Logic/IndefiniteDescription.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: IndefiniteDescription.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file provides a constructive form of indefinite description that
     allows to build choice functions; this is weaker than Hilbert's
     epsilon operator (which implies weakly classical properties) but
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 95640d67..753009e6 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: JMeq.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** John Major's Equality as proposed by Conor McBride
 
   Reference:
@@ -26,6 +24,8 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
 
 Set Elimination Schemes.
 
+Arguments JMeq_refl {A x} , [A] x.
+
 Hint Resolve JMeq_refl.
 
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
@@ -113,8 +113,7 @@ apply JMeq_refl.
 Qed.
 
 Lemma eq_dep_strictly_stronger_JMeq :
- exists U, exists P, exists p, exists q, exists x, exists y,
-  JMeq x y /\ ~ eq_dep U P p x q y.
+ exists U P p q x y, JMeq x y /\ ~ eq_dep U P p x q y.
 Proof.
 exists bool. exists (fun _ => True). exists true. exists false.
 exists I. exists I.
diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v
index 2a55f0bb..36508969 100644
--- a/theories/Logic/ProofIrrelevance.v
+++ b/theories/Logic/ProofIrrelevance.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/ProofIrrelevanceFacts.v b/theories/Logic/ProofIrrelevanceFacts.v
index 160ac2d5..6accc480 100644
--- a/theories/Logic/ProofIrrelevanceFacts.v
+++ b/theories/Logic/ProofIrrelevanceFacts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v
index 25d07fc9..d0d58e37 100644
--- a/theories/Logic/RelationalChoice.v
+++ b/theories/Logic/RelationalChoice.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RelationalChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** This file axiomatizes the relational form of the axiom of choice *)
 
 Axiom relational_choice :
diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v
index df64822d..f0876fbc 100644
--- a/theories/Logic/SetIsType.v
+++ b/theories/Logic/SetIsType.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,4 +14,4 @@
     Set: simply insert some Require Export of this file at starting
     points of the development and try to recompile...  *)
 
-Notation "'Set'" := Type (only parsing).
\ No newline at end of file
+Notation "'Set'" := Type (only parsing).