index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Logic
Mode
Name
Size
-rw-r--r--
Berardi.v
4255
log
plain
-rw-r--r--
ChoiceFacts.v
28515
log
plain
-rw-r--r--
Classical.v
632
log
plain
-rw-r--r--
ClassicalChoice.v
2071
log
plain
-rw-r--r--
ClassicalDescription.v
3068
log
plain
-rw-r--r--
ClassicalEpsilon.v
3643
log
plain
-rw-r--r--
ClassicalFacts.v
19504
log
plain
-rw-r--r--
ClassicalUniqueChoice.v
2897
log
plain
-rw-r--r--
Classical_Pred_Set.v
1602
log
plain
-rw-r--r--
Classical_Pred_Type.v
1894
log
plain
-rw-r--r--
Classical_Prop.v
3105
log
plain
-rw-r--r--
Classical_Type.v
695
log
plain
-rw-r--r--
ConstructiveEpsilon.v
5301
log
plain
-rw-r--r--
Decidable.v
4997
log
plain
-rw-r--r--
Description.v
914
log
plain
-rw-r--r--
Diaconescu.v
9695
log
plain
-rw-r--r--
Epsilon.v
2325
log
plain
-rw-r--r--
Eqdep.v
1245
log
plain
-rw-r--r--
EqdepFacts.v
9545
log
plain
-rw-r--r--
Eqdep_dec.v
8701
log
plain
-rw-r--r--
FunctionalExtensionality.v
1896
log
plain
-rw-r--r--
Hurkens.v
2628
log
plain
-rw-r--r--
IndefiniteDescription.v
1492
log
plain
-rw-r--r--
JMeq.v
3704
log
plain
-rw-r--r--
ProofIrrelevance.v
869
log
plain
-rw-r--r--
ProofIrrelevanceFacts.v
1967
log
plain
-rw-r--r--
RelationalChoice.v
814
log
plain
-rw-r--r--
SetIsType.v
956
log
plain
-rwxr-xr-x
intro.tex
247
log
plain
-rw-r--r--
vo.itarget
488
log
plain