diff options
Diffstat (limited to 'theories/Logic')
28 files changed, 53 insertions, 53 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index c4c8bbe2..d954f40c 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Berardi.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 34ebc329..60dbf3ea 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 d6c79882..3f36ff38 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-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Classical.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Classical Logic *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 08a34bc8..17b08a2f 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index f9896669..ad454a4d 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index c45bc052..52ecadaf 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 cd885592..5f4516dd 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ClassicalFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Some facts and definitions about classical logic diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index ea0898d4..fafa0b94 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalUniqueChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index b95373e5..06502d63 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Set.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Classical_Pred_Set.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** 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 32f0a6ac..bcd529f0 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Pred_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Classical_Pred_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Classical Predicate Logic on Type *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 77715ce3..c51050d5 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Prop.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Classical_Prop.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Classical Propositional Logic *) diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 2319638f..94e623bd 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Classical_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Classical_Type.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** This file is obsolete, use Classical.v instead *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 738ca1d5..004fdef3 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -1,14 +1,14 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 14641 2011-11-06 11:59:10Z herbelin $ i*) -(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z 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 diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index ac4f686b..ace50884 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -1,11 +1,11 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Decidable.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Decidable.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Properties of decidable propositions *) diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index deedf35b..c59d8460 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Description.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index ff640af7..257245cc 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Diaconescu.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index 4ec0c83d..9134b3aa 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Epsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 53b19ff6..7918061c 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep.v 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: Eqdep.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** 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 3e49c759..2d5f1537 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -1,13 +1,13 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: EqdepFacts.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index c45643e4..77908b08 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Eqdep_dec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** 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/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 4def8910..a696b6c8 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: FunctionalExtensionality.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 bb03c666..afaeb51a 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-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \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 e0537238..afca2ee1 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: IndefiniteDescription.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*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 diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 3de77074..95640d67 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: JMeq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: JMeq.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** John Major's Equality as proposed by Conor McBride diff --git a/theories/Logic/ProofIrrelevance.v b/theories/Logic/ProofIrrelevance.v index 36508969..2a55f0bb 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-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \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 6accc480..160ac2d5 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-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \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 e0a10d46..25d07fc9 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -1,12 +1,12 @@ (************************************************************************) (* 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-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: RelationalChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: RelationalChoice.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** This file axiomatizes the relational form of the axiom of choice *) diff --git a/theories/Logic/SetIsType.v b/theories/Logic/SetIsType.v index ff9ec7f6..df64822d 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-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |