aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--Berardi.v4255logplain
-rw-r--r--ChoiceFacts.v28515logplain
-rw-r--r--Classical.v632logplain
-rw-r--r--ClassicalChoice.v2071logplain
-rw-r--r--ClassicalDescription.v3068logplain
-rw-r--r--ClassicalEpsilon.v3643logplain
-rw-r--r--ClassicalFacts.v19504logplain
-rw-r--r--ClassicalUniqueChoice.v2897logplain
-rw-r--r--Classical_Pred_Set.v1602logplain
-rw-r--r--Classical_Pred_Type.v1894logplain
-rw-r--r--Classical_Prop.v3105logplain
-rw-r--r--Classical_Type.v695logplain
-rw-r--r--ConstructiveEpsilon.v5301logplain
-rw-r--r--Decidable.v4997logplain
-rw-r--r--Description.v914logplain
-rw-r--r--Diaconescu.v9695logplain
-rw-r--r--Epsilon.v2325logplain
-rw-r--r--Eqdep.v1245logplain
-rw-r--r--EqdepFacts.v9545logplain
-rw-r--r--Eqdep_dec.v8701logplain
-rw-r--r--FunctionalExtensionality.v1896logplain
-rw-r--r--Hurkens.v2628logplain
-rw-r--r--IndefiniteDescription.v1492logplain
-rw-r--r--JMeq.v3704logplain
-rw-r--r--ProofIrrelevance.v869logplain
-rw-r--r--ProofIrrelevanceFacts.v1967logplain
-rw-r--r--RelationalChoice.v814logplain
-rw-r--r--SetIsType.v956logplain
-rwxr-xr-xintro.tex247logplain
-rw-r--r--vo.itarget488logplain