aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--Berardi.v4280logplain
-rw-r--r--ChoiceFacts.v48510logplain
-rw-r--r--Classical.v816logplain
-rw-r--r--ClassicalChoice.v2207logplain
-rw-r--r--ClassicalDescription.v3204logplain
-rw-r--r--ClassicalEpsilon.v3826logplain
-rw-r--r--ClassicalFacts.v26620logplain
-rw-r--r--ClassicalUniqueChoice.v3274logplain
-rw-r--r--Classical_Pred_Type.v2113logplain
-rw-r--r--Classical_Prop.v3404logplain
-rw-r--r--ConstructiveEpsilon.v9316logplain
-rw-r--r--Decidable.v5492logplain
-rw-r--r--Description.v1050logplain
-rw-r--r--Diaconescu.v9867logplain
-rw-r--r--Epsilon.v2461logplain
-rw-r--r--Eqdep.v1571logplain
-rw-r--r--EqdepFacts.v15794logplain
-rw-r--r--Eqdep_dec.v11754logplain
-rw-r--r--ExtensionalFunctionRepresentative.v1366logplain
-rw-r--r--ExtensionalityFacts.v4653logplain
-rw-r--r--FinFun.v12556logplain
-rw-r--r--FunctionalExtensionality.v9078logplain
-rw-r--r--Hurkens.v22893logplain
-rw-r--r--IndefiniteDescription.v1628logplain
-rw-r--r--JMeq.v3898logplain
-rw-r--r--ProofIrrelevance.v1019logplain
-rw-r--r--ProofIrrelevanceFacts.v2115logplain
-rw-r--r--PropExtensionality.v1031logplain
-rw-r--r--PropExtensionalityFacts.v4110logplain
-rw-r--r--PropFacts.v1843logplain
-rw-r--r--RelationalChoice.v950logplain
-rw-r--r--SetIsType.v1107logplain
-rw-r--r--SetoidChoice.v2391logplain
-rw-r--r--WKL.v9618logplain
-rw-r--r--WeakFan.v3508logplain