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.v
446
log
plain
-rw-r--r--
Case1.v
335
log
plain
-rw-r--r--
Case10.v
738
log
plain
-rw-r--r--
Case11.v
341
log
plain
-rw-r--r--
Case12.v
2074
log
plain
-rw-r--r--
Case13.v
1725
log
plain
-rw-r--r--
Case14.v
510
log
plain
-rw-r--r--
Case15.v
1318
log
plain
-rw-r--r--
Case16.v
405
log
plain
-rw-r--r--
Case17.v
1850
log
plain
-rw-r--r--
Case18.v
214
log
plain
-rw-r--r--
Case2.v
306
log
plain
-rw-r--r--
Case5.v
365
log
plain
-rw-r--r--
Case6.v
583
log
plain
-rw-r--r--
Case7.v
474
log
plain
-rw-r--r--
Case8.v
338
log
plain
-rw-r--r--
Case9.v
2237
log
plain
-rw-r--r--
CaseAlias.v
386
log
plain
-rw-r--r--
Cases.v
38183
log
plain
-rw-r--r--
CasesDep.v
10927
log
plain
-rw-r--r--
Check.v
795
log
plain
-rw-r--r--
Conjecture.v
231
log
plain
-rw-r--r--
DHyp.v
1
log
plain
-rw-r--r--
Decompose.v
218
log
plain
-rw-r--r--
DiscrR.v
435
log
plain
-rw-r--r--
Discriminate.v
206
log
plain
-rw-r--r--
Field.v
1699
log
plain
-rw-r--r--
Fixpoint.v
981
log
plain
-rw-r--r--
Fourier.v
283
log
plain
-rw-r--r--
Funind.v
8846
log
plain
-rw-r--r--
Generalize.v
176
log
plain
-rw-r--r--
Hints.v
1261
log
plain
-rw-r--r--
ImplicitTactic.v
549
log
plain
-rw-r--r--
Inductive.v
1427
log
plain
-rw-r--r--
Injection.v
928
log
plain
-rw-r--r--
Inversion.v
2676
log
plain
-rw-r--r--
LetIn.v
356
log
plain
-rw-r--r--
MatchFail.v
822
log
plain
-rw-r--r--
Mod_ltac.v
302
log
plain
-rw-r--r--
Mod_params.v
1445
log
plain
-rw-r--r--
Mod_strengthen.v
963
log
plain
-rw-r--r--
Mod_type.v
269
log
plain
-rw-r--r--
NatRing.v
133
log
plain
-rw-r--r--
Notations.v
286
log
plain
-rw-r--r--
Omega.v
2201
log
plain
-rw-r--r--
Omega0.v
2467
log
plain
-rw-r--r--
Omega2.v
764
log
plain
-rw-r--r--
PPFix.v
207
log
plain
-rw-r--r--
Print.v
282
log
plain
-rw-r--r--
Projection.v
1154
log
plain
-rw-r--r--
ROmega.v
2356
log
plain
-rw-r--r--
ROmega0.v
2533
log
plain
-rw-r--r--
ROmega2.v
775
log
plain
-rw-r--r--
RecTutorial.v
25255
log
plain
-rw-r--r--
Record.v
106
log
plain
-rw-r--r--
Reg.v
3094
log
plain
-rw-r--r--
Remark.v
172
log
plain
-rw-r--r--
Rename.v
220
log
plain
-rw-r--r--
Require.v
88
log
plain
-rw-r--r--
Reset.v
77
log
plain
-rw-r--r--
Scopes.v
157
log
plain
-rw-r--r--
Simplify_eq.v
258
log
plain
-rw-r--r--
Tauto.v
5202
log
plain
-rw-r--r--
TestRefine.v
4406
log
plain
-rw-r--r--
Try.v
182
log
plain
-rw-r--r--
autorewritein.v
527
log
plain
-rw-r--r--
cc.v
1759
log
plain
-rw-r--r--
coercions.v
724
log
plain
-rw-r--r--
coqbugs0181.v
211
log
plain
-rw-r--r--
destruct.v
489
log
plain
-rw-r--r--
eauto.v
1868
log
plain
-rw-r--r--
eqdecide.v
912
log
plain
-rw-r--r--
evars.v
1991
log
plain
-rw-r--r--
extraction.v
112
log
plain
-rw-r--r--
fix.v
1732
log
plain
-rw-r--r--
if.v
366
log
plain
-rw-r--r--
implicit.v
786
log
plain
-rw-r--r--
import_lib.v
3467
log
plain
-rw-r--r--
import_mod.v
993
log
plain
-rw-r--r--
inds_type_sec.v
594
log
plain
-rw-r--r--
induct.v
698
log
plain
-rw-r--r--
intros.v
168
log
plain
-rw-r--r--
ltac.v
3151
log
plain
-rw-r--r--
mutual_ind.v
1604
log
plain
-rw-r--r--
options.v
686
log
plain
-rw-r--r--
params_ind.v
93
log
plain
-rw-r--r--
refine.v
1939
log
plain
-rw-r--r--
rewrite.v
530
log
plain
-rw-r--r--
set.v
90
log
plain
-rw-r--r--
setoid_test.v
1953
log
plain
-rw-r--r--
setoid_test2.v
8151
log
plain
-rw-r--r--
setoid_test_function_space.v
1387
log
plain
-rw-r--r--
simpl.v
655
log
plain
-rw-r--r--
unfold.v
644
log
plain
-rw-r--r--
unicode_utf8.v
372
log
plain
-rw-r--r--
univers.v
1646
log
plain