diff options
Diffstat (limited to 'theories/Logic')
24 files changed, 27 insertions, 27 deletions
diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 7d9fb802..c4c8bbe2 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Berardi.v 13323 2010-07-24 15:57:30Z 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 959670cb..34ebc329 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 12363 2009-09-28 15:04:07Z letouzey $ i*) +(*i $Id: ChoiceFacts.v 13323 2010-07-24 15:57:30Z 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 b2cca5c2..d6c79882 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Logic *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 50ce871b..08a34bc8 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalChoice.v 13323 2010-07-24 15:57:30Z 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 793c6ab7..f9896669 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$ i*) +(*i $Id: ClassicalDescription.v 13323 2010-07-24 15:57:30Z 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 53989d07..c45bc052 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalEpsilon.v 13323 2010-07-24 15:57:30Z 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 c5822bac..cd885592 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$ i*) +(*i $Id: ClassicalFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Some facts and definitions about classical logic diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 6c1c68cf..ea0898d4 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalUniqueChoice.v 13323 2010-07-24 15:57:30Z 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 3f30abe5..b95373e5 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Pred_Set.v 13323 2010-07-24 15:57:30Z 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 638c58d2..32f0a6ac 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Pred_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Predicate Logic on Type *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 91392ca6..77715ce3 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Prop.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Propositional Logic *) diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 2f5c9726..2319638f 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file is obsolete, use Classical.v instead *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 90aa0f30..738ca1d5 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) -(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z 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 df9acbcc..ac4f686b 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Decidable.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Properties of decidable propositions *) diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index c569dc46..deedf35b 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Description.v 13323 2010-07-24 15:57:30Z 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 4c4785cf..ff640af7 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$ i*) +(*i $Id: Diaconescu.v 13323 2010-07-24 15:57:30Z 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 9cea8dfd..4ec0c83d 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Epsilon.v 13323 2010-07-24 15:57:30Z 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 ed9d1a9f..53b19ff6 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Eqdep.v 13332 2010-07-26 22:12:43Z msozeau $ i*) (** This file axiomatizes the invariance by substitution of reflexive equality proofs [[Streicher93]] and exports its consequences, such @@ -31,5 +31,5 @@ Export EqdepTheory. (** Exported hints *) -Hint Resolve eq_dep_eq: core v62. -Hint Resolve inj_pair2 inj_pairT2: core. +Hint Resolve eq_dep_eq: eqdep v62. +Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 15a36dd4..3e49c759 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: EqdepFacts.v 13323 2010-07-24 15:57:30Z 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 0ad7e909..c45643e4 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Eqdep_dec.v 13323 2010-07-24 15:57:30Z 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 5e9953d4..4def8910 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: FunctionalExtensionality.v 13323 2010-07-24 15:57:30Z 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/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 05c04952..e0537238 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: IndefiniteDescription.v 13323 2010-07-24 15:57:30Z 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 06903c3b..3de77074 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: JMeq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** John Major's Equality as proposed by Conor McBride diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 85da26b3..e0a10d46 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RelationalChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file axiomatizes the relational form of the axiom of choice *) |