Logic « theories - debian-coq - Debian packaging for Coq

Mode	Name	Size
-rw-r--r--	Berardi.v	4305	log plain
-rw-r--r--	ChoiceFacts.v	26640	log plain
-rw-r--r--	Classical.v	678	log plain
-rw-r--r--	ClassicalChoice.v	2127	log plain
-rw-r--r--	ClassicalDescription.v	3133	log plain
-rw-r--r--	ClassicalEpsilon.v	3679	log plain
-rw-r--r--	ClassicalFacts.v	19581	log plain
-rw-r--r--	ClassicalUniqueChoice.v	2925	log plain
-rw-r--r--	Classical_Pred_Set.v	1657	log plain
-rw-r--r--	Classical_Pred_Type.v	1951	log plain
-rw-r--r--	Classical_Prop.v	3163	log plain
-rw-r--r--	Classical_Type.v	746	log plain
-rw-r--r--	ConstructiveEpsilon.v	5333	log plain
-rw-r--r--	Decidable.v	5062	log plain
-rw-r--r--	DecidableType.v	4532	log plain
-rw-r--r--	DecidableTypeEx.v	3533	log plain
-rw-r--r--	Description.v	967	log plain
-rw-r--r--	Diaconescu.v	9765	log plain
-rw-r--r--	Epsilon.v	2378	log plain
-rw-r--r--	Eqdep.v	1259	log plain
-rw-r--r--	EqdepFacts.v	9613	log plain
-rw-r--r--	Eqdep_dec.v	8772	log plain
-rw-r--r--	FunctionalExtensionality.v	1968	log plain
-rw-r--r--	Hurkens.v	2621	log plain
-rw-r--r--	IndefiniteDescription.v	1556	log plain
-rw-r--r--	JMeq.v	3036	log plain
-rw-r--r--	ProofIrrelevance.v	869	log plain
-rw-r--r--	ProofIrrelevanceFacts.v	1969	log plain
-rw-r--r--	RelationalChoice.v	871	log plain
-rw-r--r--	SetIsType.v	956	log plain
-rwxr-xr-x	intro.tex	247	log plain