aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--Berardi.v4258logplain
-rw-r--r--ChoiceFacts.v26588logplain
-rw-r--r--Classical.v632logplain
-rw-r--r--ClassicalChoice.v2071logplain
-rw-r--r--ClassicalDescription.v3057logplain
-rw-r--r--ClassicalEpsilon.v3622logplain
-rw-r--r--ClassicalFacts.v19511logplain
-rw-r--r--ClassicalUniqueChoice.v2863logplain
-rw-r--r--Classical_Pred_Set.v1602logplain
-rw-r--r--Classical_Pred_Type.v1895logplain
-rw-r--r--Classical_Prop.v3109logplain
-rw-r--r--Classical_Type.v695logplain
-rw-r--r--ConstructiveEpsilon.v5273logplain
-rw-r--r--Decidable.v4860logplain
-rw-r--r--DecidableType.v4478logplain
-rw-r--r--DecidableTypeEx.v3733logplain
-rw-r--r--Description.v915logplain
-rw-r--r--Diaconescu.v9699logplain
-rw-r--r--Epsilon.v2330logplain
-rw-r--r--Eqdep.v1217logplain
-rw-r--r--EqdepFacts.v9578logplain
-rw-r--r--Eqdep_dec.v8724logplain
-rw-r--r--Hurkens.v2621logplain
-rw-r--r--IndefiniteDescription.v1494logplain
-rw-r--r--JMeq.v2992logplain
-rw-r--r--ProofIrrelevance.v869logplain
-rw-r--r--ProofIrrelevanceFacts.v1969logplain
-rw-r--r--RelationalChoice.v815logplain
-rw-r--r--SetIsType.v956logplain
-rwxr-xr-xintro.tex247logplain