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

Mode	Name	Size
-rw-r--r--	Berardi.v	4303	log plain
-rw-r--r--	ChoiceFacts.v	28515	log plain
-rw-r--r--	Classical.v	682	log plain
-rw-r--r--	ClassicalChoice.v	2127	log plain
-rw-r--r--	ClassicalDescription.v	3129	log plain
-rw-r--r--	ClassicalEpsilon.v	3700	log plain
-rw-r--r--	ClassicalFacts.v	19559	log plain
-rw-r--r--	ClassicalUniqueChoice.v	3199	log plain
-rw-r--r--	Classical_Pred_Set.v	1661	log plain
-rw-r--r--	Classical_Pred_Type.v	1954	log plain
-rw-r--r--	Classical_Prop.v	3160	log plain
-rw-r--r--	Classical_Type.v	750	log plain
-rw-r--r--	ConstructiveEpsilon.v	8154	log plain
-rw-r--r--	Decidable.v	5047	log plain
-rw-r--r--	Description.v	966	log plain
-rw-r--r--	Diaconescu.v	9746	log plain
-rw-r--r--	Epsilon.v	2373	log plain
-rw-r--r--	Eqdep.v	1293	log plain
-rw-r--r--	EqdepFacts.v	9596	log plain
-rw-r--r--	Eqdep_dec.v	8939	log plain
-rw-r--r--	FunctionalExtensionality.v	1947	log plain
-rw-r--r--	Hurkens.v	2628	log plain
-rw-r--r--	IndefiniteDescription.v	1554	log plain
-rw-r--r--	JMeq.v	3749	log plain
-rw-r--r--	ProofIrrelevance.v	869	log plain
-rw-r--r--	ProofIrrelevanceFacts.v	1967	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
-rw-r--r--	vo.itarget	488	log plain