index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
success
Mode
Name
Size
-rw-r--r--
Abstract.v8
445
log
plain
-rw-r--r--
Case1.v
400
log
plain
-rw-r--r--
Case10.v
764
log
plain
-rw-r--r--
Case11.v
285
log
plain
-rw-r--r--
Case12.v
1442
log
plain
-rw-r--r--
Case13.v
959
log
plain
-rw-r--r--
Case14.v
489
log
plain
-rw-r--r--
Case15.v
1303
log
plain
-rw-r--r--
Case16.v
388
log
plain
-rw-r--r--
Case17.v
1893
log
plain
-rw-r--r--
Case2.v
339
log
plain
-rw-r--r--
Case5.v
351
log
plain
-rw-r--r--
Case6.v
597
log
plain
-rw-r--r--
Case7.v
459
log
plain
-rw-r--r--
Case9.v
2270
log
plain
-rw-r--r--
CaseAlias.v
380
log
plain
-rw-r--r--
Cases.v
46156
log
plain
-rw-r--r--
CasesDep.v
10886
log
plain
-rw-r--r--
Check.v
795
log
plain
-rw-r--r--
Conjecture.v
210
log
plain
-rw-r--r--
DHyp.v
217
log
plain
-rw-r--r--
Decompose.v
187
log
plain
-rw-r--r--
Destruct.v
236
log
plain
-rw-r--r--
DiscrR.v
395
log
plain
-rw-r--r--
Discriminate.v
196
log
plain
-rw-r--r--
Field.v
1498
log
plain
-rw-r--r--
Fourier.v
300
log
plain
-rw-r--r--
Funind.v
9863
log
plain
-rw-r--r--
Generalize.v
137
log
plain
-rw-r--r--
Hints.v
1559
log
plain
-rw-r--r--
Inductive.v
1057
log
plain
-rw-r--r--
Injection.v
814
log
plain
-rw-r--r--
Inversion.v
2319
log
plain
-rw-r--r--
LetIn.v
314
log
plain
-rw-r--r--
MatchFail.v
958
log
plain
-rw-r--r--
Mod_ltac.v
264
log
plain
-rw-r--r--
Mod_params.v
1325
log
plain
-rw-r--r--
Mod_strengthen.v
889
log
plain
-rw-r--r--
NatRing.v
144
log
plain
-rw-r--r--
Omega.v
1702
log
plain
-rw-r--r--
PPFix.v8
206
log
plain
-rw-r--r--
Print.v
297
log
plain
-rw-r--r--
Projection.v
1059
log
plain
-rw-r--r--
Record.v
105
log
plain
-rw-r--r--
Reg.v
2837
log
plain
-rw-r--r--
Remark.v
172
log
plain
-rw-r--r--
Rename.v
78
log
plain
-rw-r--r--
Require.v
85
log
plain
-rw-r--r--
Scopes.v
157
log
plain
-rw-r--r--
Simplify_eq.v
241
log
plain
-rw-r--r--
Tauto.v
4831
log
plain
-rw-r--r--
Try.v
176
log
plain
-rw-r--r--
cc.v
1721
log
plain
-rw-r--r--
coercions.v
202
log
plain
-rw-r--r--
coqbugs0181.v
202
log
plain
-rw-r--r--
eauto.v
1706
log
plain
-rw-r--r--
eqdecide.v
838
log
plain
-rw-r--r--
evars.v
802
log
plain
-rw-r--r--
fix.v
1661
log
plain
-rw-r--r--
if.v
154
log
plain
-rw-r--r--
implicit.v
741
log
plain
-rw-r--r--
import_lib.v
3550
log
plain
-rw-r--r--
import_mod.v
981
log
plain
-rw-r--r--
inds_type_sec.v
590
log
plain
-rw-r--r--
induct.v
693
log
plain
-rw-r--r--
ltac.v
1744
log
plain
-rw-r--r--
mutual_ind.v
1515
log
plain
-rw-r--r--
options.v
662
log
plain
-rw-r--r--
refine.v
498
log
plain
-rw-r--r--
setoid_test.v
1708
log
plain
-rw-r--r--
unfold.v
648
log
plain
-rw-r--r--
univers.v
305
log
plain