index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
failure
Mode
Name
Size
-rw-r--r--
Case1.v
61
log
plain
-rw-r--r--
Case10.v
116
log
plain
-rw-r--r--
Case11.v
118
log
plain
-rw-r--r--
Case12.v
142
log
plain
-rw-r--r--
Case13.v
145
log
plain
-rw-r--r--
Case14.v
204
log
plain
-rw-r--r--
Case15.v
155
log
plain
-rw-r--r--
Case16.v
199
log
plain
-rw-r--r--
Case2.v
267
log
plain
-rw-r--r--
Case3.v
194
log
plain
-rw-r--r--
Case4.v
141
log
plain
-rw-r--r--
Case5.v
164
log
plain
-rw-r--r--
Case6.v
192
log
plain
-rw-r--r--
Case7.v
456
log
plain
-rw-r--r--
Case8.v
178
log
plain
-rw-r--r--
Case9.v
221
log
plain
-rw-r--r--
ClearBody.v
246
log
plain
-rw-r--r--
ImportedCoercion.v
126
log
plain
-rw-r--r--
Notations.v
148
log
plain
-rw-r--r--
Reordering.v
189
log
plain
-rw-r--r--
Sections.v
58
log
plain
-rw-r--r--
Tauto.v
1080
log
plain
-rw-r--r--
Uminus.v
530
log
plain
-rw-r--r--
autorewritein.v
397
log
plain
-rw-r--r--
cases.v
155
log
plain
-rw-r--r--
check.v
45
log
plain
-rw-r--r--
circular_subtyping.v
299
log
plain
-rw-r--r--
clash_cons.v
810
log
plain
-rw-r--r--
clashes.v
210
log
plain
-rw-r--r--
cofixpoint.v
393
log
plain
-rw-r--r--
coqbugs0266.v
178
log
plain
-rw-r--r--
evar1.v
129
log
plain
-rw-r--r--
evarclear1.v
250
log
plain
-rw-r--r--
evarclear2.v
217
log
plain
-rw-r--r--
evarlemma.v
93
log
plain
-rw-r--r--
fixpoint1.v
778
log
plain
-rw-r--r--
fixpoint2.v
104
log
plain
-rw-r--r--
fixpoint3.v
335
log
plain
-rw-r--r--
fixpoint4.v
557
log
plain
-rw-r--r--
fixpointeta.v
1969
log
plain
-rw-r--r--
guard.v
1015
log
plain
-rw-r--r--
guard_cofix.v
1165
log
plain
-rw-r--r--
illtype1.v
693
log
plain
-rw-r--r--
inductive.v
1037
log
plain
-rw-r--r--
int63.v
317
log
plain
-rw-r--r--
ltac1.v
180
log
plain
-rw-r--r--
ltac2.v
164
log
plain
-rw-r--r--
ltac4.v
158
log
plain
-rw-r--r--
pattern.v
207
log
plain
-rw-r--r--
positivity.v
1585
log
plain
-rw-r--r--
proofirrelevance.v
405
log
plain
-rw-r--r--
prop_set_proof_irrelevance.v
327
log
plain
-rw-r--r--
redef.v
728
log
plain
-rw-r--r--
rewrite_in_goal.v
111
log
plain
-rw-r--r--
rewrite_in_hyp.v
127
log
plain
-rw-r--r--
rewrite_in_hyp2.v
333
log
plain
-rw-r--r--
search.v
725
log
plain
-rw-r--r--
sortelim.v
4162
log
plain
-rw-r--r--
subterm.v
1050
log
plain
-rw-r--r--
subterm2.v
1249
log
plain
-rw-r--r--
subterm3.v
824
log
plain
-rw-r--r--
subtyping.v
332
log
plain
-rw-r--r--
subtyping2.v
6430
log
plain
-rw-r--r--
uip_loop.v
564
log
plain
-rw-r--r--
univ_include.v
534
log
plain
-rw-r--r--
universes.v
108
log
plain
-rw-r--r--
universes3.v
1188
log
plain
-rw-r--r--
universes_buraliforti.v
6296
log
plain
-rw-r--r--
universes_buraliforti_redef.v
6844
log
plain
-rw-r--r--
universes_sections1.v
205
log
plain
-rw-r--r--
universes_sections2.v
223
log
plain
