aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--Berardi.v4241logplain
-rw-r--r--ChoiceFacts.v28449logplain
-rw-r--r--Classical.v666logplain
-rw-r--r--ClassicalChoice.v2057logplain
-rw-r--r--ClassicalDescription.v3054logplain
-rw-r--r--ClassicalEpsilon.v3629logplain
-rw-r--r--ClassicalFacts.v19490logplain
-rw-r--r--ClassicalUniqueChoice.v3123logplain
-rw-r--r--Classical_Pred_Set.v1680logplain
-rw-r--r--Classical_Pred_Type.v1995logplain
-rw-r--r--Classical_Prop.v3297logplain
-rw-r--r--Classical_Type.v681logplain
-rw-r--r--ConstructiveEpsilon.v9205logplain
-rw-r--r--Decidable.v4981logplain
-rw-r--r--Description.v900logplain
-rw-r--r--Diaconescu.v9685logplain
-rw-r--r--Epsilon.v2311logplain
-rw-r--r--Eqdep.v1425logplain
-rw-r--r--EqdepFacts.v11973logplain
-rw-r--r--Eqdep_dec.v8987logplain
-rw-r--r--ExtensionalityFacts.v4503logplain
-rw-r--r--FunctionalExtensionality.v1868logplain
-rw-r--r--Hurkens.v2628logplain
-rw-r--r--IndefiniteDescription.v1478logplain
-rw-r--r--JMeq.v3684logplain
-rw-r--r--ProofIrrelevance.v869logplain
-rw-r--r--ProofIrrelevanceFacts.v1967logplain
-rw-r--r--RelationalChoice.v800logplain
-rw-r--r--SetIsType.v957logplain
-rwxr-xr-xintro.tex247logplain
-rw-r--r--vo.itarget488logplain