aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--Berardi.v4130logplain
-rw-r--r--ChoiceFacts.v47150logplain
-rw-r--r--Classical.v666logplain
-rw-r--r--ClassicalChoice.v2057logplain
-rw-r--r--ClassicalDescription.v3054logplain
-rw-r--r--ClassicalEpsilon.v3629logplain
-rw-r--r--ClassicalFacts.v26470logplain
-rw-r--r--ClassicalUniqueChoice.v3124logplain
-rw-r--r--Classical_Pred_Type.v1963logplain
-rw-r--r--Classical_Prop.v3270logplain
-rw-r--r--ConstructiveEpsilon.v9166logplain
-rw-r--r--Decidable.v5342logplain
-rw-r--r--Description.v900logplain
-rw-r--r--Diaconescu.v9684logplain
-rw-r--r--Epsilon.v2311logplain
-rw-r--r--Eqdep.v1421logplain
-rw-r--r--EqdepFacts.v15644logplain
-rw-r--r--Eqdep_dec.v11604logplain
-rw-r--r--ExtensionalFunctionRepresentative.v1216logplain
-rw-r--r--ExtensionalityFacts.v4503logplain
-rw-r--r--FinFun.v12406logplain
-rw-r--r--FunctionalExtensionality.v8958logplain
-rw-r--r--Hurkens.v22743logplain
-rw-r--r--IndefiniteDescription.v1478logplain
-rw-r--r--JMeq.v3748logplain
-rw-r--r--ProofIrrelevance.v869logplain
-rw-r--r--ProofIrrelevanceFacts.v1965logplain
-rw-r--r--PropExtensionality.v881logplain
-rw-r--r--PropExtensionalityFacts.v3960logplain
-rw-r--r--PropFacts.v1693logplain
-rw-r--r--RelationalChoice.v800logplain
-rw-r--r--SetIsType.v957logplain
-rw-r--r--SetoidChoice.v2241logplain
-rw-r--r--WKL.v9468logplain
-rw-r--r--WeakFan.v3358logplain
-rw-r--r--vo.itarget601logplain