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
56
log
plain
-rw-r--r--
Case10.v
111
log
plain
-rw-r--r--
Case11.v
113
log
plain
-rw-r--r--
Case12.v
137
log
plain
-rw-r--r--
Case13.v
140
log
plain
-rw-r--r--
Case14.v
199
log
plain
-rw-r--r--
Case15.v
150
log
plain
-rw-r--r--
Case16.v
194
log
plain
-rw-r--r--
Case2.v
262
log
plain
-rw-r--r--
Case3.v
189
log
plain
-rw-r--r--
Case4.v
136
log
plain
-rw-r--r--
Case5.v
159
log
plain
-rw-r--r--
Case6.v
187
log
plain
-rw-r--r--
Case7.v
451
log
plain
-rw-r--r--
Case8.v
173
log
plain
-rw-r--r--
Case9.v
224
log
plain
-rw-r--r--
ClearBody.v
234
log
plain
-rw-r--r--
ImportedCoercion.v
121
log
plain
-rw-r--r--
Notations.v
143
log
plain
-rw-r--r--
Reordering.v
177
log
plain
-rw-r--r--
Sections.v
35
log
plain
-rw-r--r--
Tauto.v
918
log
plain
-rw-r--r--
Uminus.v
1422
log
plain
-rw-r--r--
autorewritein.v
388
log
plain
-rw-r--r--
cases.v
150
log
plain
-rw-r--r--
check.v
49
log
plain
-rw-r--r--
circular_subtyping1.v
223
log
plain
-rw-r--r--
circular_subtyping2.v
235
log
plain
-rw-r--r--
clash_cons.v
655
log
plain
-rw-r--r--
clashes.v
198
log
plain
-rw-r--r--
coqbugs0266.v
159
log
plain
-rw-r--r--
evar1.v
124
log
plain
-rw-r--r--
evarclear1.v
239
log
plain
-rw-r--r--
evarclear2.v
205
log
plain
-rw-r--r--
evarlemma.v
88
log
plain
-rw-r--r--
fixpoint1.v
619
log
plain
-rw-r--r--
fixpoint2.v
92
log
plain
-rw-r--r--
fixpoint3.v
330
log
plain
-rw-r--r--
fixpoint4.v
552
log
plain
-rw-r--r--
guard.v
856
log
plain
-rw-r--r--
illtype1.v
538
log
plain
-rw-r--r--
inductive1.v
179
log
plain
-rw-r--r--
inductive2.v
179
log
plain
-rw-r--r--
inductive3.v
253
log
plain
-rw-r--r--
inductive4.v
521
log
plain
-rw-r--r--
ltac1.v
168
log
plain
-rw-r--r--
ltac2.v
152
log
plain
-rw-r--r--
ltac4.v
147
log
plain
-rw-r--r--
pattern.v
195
log
plain
-rw-r--r--
positivity.v
571
log
plain
-rw-r--r--
proofirrelevance.v
411
log
plain
-rw-r--r--
prop-set-proof-irrelevance.v
311
log
plain
-rw-r--r--
redef.v
573
log
plain
-rw-r--r--
rewrite_in_goal.v
99
log
plain
-rw-r--r--
rewrite_in_hyp.v
115
log
plain
-rw-r--r--
rewrite_in_hyp2.v
321
log
plain
-rw-r--r--
search.v
570
log
plain
-rw-r--r--
subtyping.v
251
log
plain
-rw-r--r--
subtyping2.v
6425
log
plain
-rw-r--r--
univ_include.v
523
log
plain
-rw-r--r--
universes-buraliforti-redef.v
6825
log
plain
-rw-r--r--
universes-buraliforti.v
6291
log
plain
-rw-r--r--
universes-sections1.v
200
log
plain
-rw-r--r--
universes-sections2.v
218
log
plain
-rw-r--r--
universes.v
103
log
plain
-rw-r--r--
universes3.v
1183
log
plain
