index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
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
239
log
plain
-rw-r--r--
ImportedCoercion.v
126
log
plain
-rw-r--r--
Notations.v
148
log
plain
-rw-r--r--
Reordering.v
182
log
plain
-rw-r--r--
Sections.v
44
log
plain
-rw-r--r--
Tauto.v
1073
log
plain
-rw-r--r--
Uminus.v
530
log
plain
-rw-r--r--
autorewritein.v
393
log
plain
-rw-r--r--
cases.v
155
log
plain
-rw-r--r--
check.v
54
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
203
log
plain
-rw-r--r--
cofixpoint.v
393
log
plain
-rw-r--r--
coqbugs0266.v
164
log
plain
-rw-r--r--
evar1.v
129
log
plain
-rw-r--r--
evarclear1.v
244
log
plain
-rw-r--r--
evarclear2.v
210
log
plain
-rw-r--r--
evarlemma.v
93
log
plain
-rw-r--r--
fixpoint1.v
778
log
plain
-rw-r--r--
fixpoint2.v
97
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-cofix.v
1165
log
plain
-rw-r--r--
guard.v
1015
log
plain
-rw-r--r--
illtype1.v
693
log
plain
-rw-r--r--
inductive.v
1037
log
plain
-rw-r--r--
int31.v
305
log
plain
-rw-r--r--
ltac1.v
173
log
plain
-rw-r--r--
ltac2.v
157
log
plain
-rw-r--r--
ltac4.v
152
log
plain
-rw-r--r--
pattern.v
200
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
320
log
plain
-rw-r--r--
redef.v
728
log
plain
-rw-r--r--
rewrite_in_goal.v
104
log
plain
-rw-r--r--
rewrite_in_hyp.v
120
log
plain
-rw-r--r--
rewrite_in_hyp2.v
326
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
256
log
plain
-rw-r--r--
subtyping2.v
6430
log
plain
-rw-r--r--
univ_include.v
534
log
plain
-rw-r--r--
universes-buraliforti-redef.v
6844
log
plain
-rw-r--r--
universes-buraliforti.v
6296
log
plain
-rw-r--r--
universes-sections1.v
205
log
plain
-rw-r--r--
universes-sections2.v
223
log
plain
-rw-r--r--
universes.v
108
log
plain
-rw-r--r--
universes3.v
1188
log
plain
