aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Logic
ModeNameSize
-rw-r--r--.cvsignore5logplain
-rw-r--r--Berardi.v4251logplain
-rw-r--r--ChoiceFacts.v4813logplain
-rwxr-xr-xClassical.v630logplain
-rw-r--r--ClassicalChoice.v1252logplain
-rw-r--r--ClassicalDescription.v2606logplain
-rw-r--r--ClassicalFacts.v7566logplain
-rwxr-xr-xClassical_Pred_Set.v1602logplain
-rwxr-xr-xClassical_Pred_Type.v1832logplain
-rwxr-xr-xClassical_Prop.v2249logplain
-rwxr-xr-xClassical_Type.v695logplain
-rw-r--r--Decidable.v1889logplain
-rw-r--r--Diaconescu.v4292logplain
-rwxr-xr-xEqdep.v5289logplain
-rw-r--r--Eqdep_dec.v3170logplain
-rw-r--r--Hurkens.v2621logplain
-rw-r--r--JMeq.v2116logplain
-rw-r--r--ProofIrrelevance.v4027logplain
-rw-r--r--RelationalChoice.v876logplain
-rwxr-xr-xintro.tex247logplain