Logic « theories - coq - The formal proof system

Mode	Name	Size
-rw-r--r--	Berardi.v	4440	log plain
-rw-r--r--	ChoiceFacts.v	48512	log plain
-rw-r--r--	Classical.v	816	log plain
-rw-r--r--	ClassicalChoice.v	2207	log plain
-rw-r--r--	ClassicalDescription.v	3204	log plain
-rw-r--r--	ClassicalEpsilon.v	3826	log plain
-rw-r--r--	ClassicalFacts.v	27333	log plain
-rw-r--r--	ClassicalUniqueChoice.v	3274	log plain
-rw-r--r--	Classical_Pred_Type.v	2113	log plain
-rw-r--r--	Classical_Prop.v	3448	log plain
-rw-r--r--	ConstructiveEpsilon.v	10572	log plain
-rw-r--r--	Decidable.v	6019	log plain
-rw-r--r--	Description.v	1050	log plain
-rw-r--r--	Diaconescu.v	9836	log plain
-rw-r--r--	Epsilon.v	2461	log plain
-rw-r--r--	Eqdep.v	1591	log plain
-rw-r--r--	EqdepFacts.v	15617	log plain
-rw-r--r--	Eqdep_dec.v	11658	log plain
-rw-r--r--	ExtensionalFunctionRepresentative.v	1366	log plain
-rw-r--r--	ExtensionalityFacts.v	4677	log plain
-rw-r--r--	FinFun.v	12556	log plain
-rw-r--r--	FunctionalExtensionality.v	9099	log plain
-rw-r--r--	HLevels.v	5207	log plain
-rw-r--r--	Hurkens.v	22899	log plain
-rw-r--r--	IndefiniteDescription.v	1628	log plain
-rw-r--r--	JMeq.v	4231	log plain
-rw-r--r--	ProofIrrelevance.v	1074	log plain
-rw-r--r--	ProofIrrelevanceFacts.v	2120	log plain
-rw-r--r--	PropExtensionality.v	1031	log plain
-rw-r--r--	PropExtensionalityFacts.v	4110	log plain
-rw-r--r--	PropFacts.v	1843	log plain
-rw-r--r--	RelationalChoice.v	950	log plain
-rw-r--r--	SetIsType.v	1107	log plain
-rw-r--r--	SetoidChoice.v	2391	log plain
-rw-r--r--	StrictProp.v	1342	log plain
-rw-r--r--	WKL.v	9618	log plain
-rw-r--r--	WeakFan.v	3512	log plain