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--
AdvancedCanonicalStructure.v
2979
log
plain
-rw-r--r--
CanonicalStructure.v
713
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
2149
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
513
log
plain
-rw-r--r--
Case19.v
272
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-bug1834.v
379
log
plain
-rw-r--r--
Cases.v
38268
log
plain
-rw-r--r--
CasesDep.v
12108
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
571
log
plain
-rw-r--r--
Equations.v
10700
log
plain
-rw-r--r--
Field.v
1906
log
plain
-rw-r--r--
Fixpoint.v
1400
log
plain
-rw-r--r--
Fourier.v
283
log
plain
-rw-r--r--
Funind.v
10176
log
plain
-rw-r--r--
Generalization.v
253
log
plain
-rw-r--r--
Generalize.v
176
log
plain
-rw-r--r--
Hints.v
1261
log
plain
-rw-r--r--
ImplicitArguments.v
545
log
plain
-rw-r--r--
ImplicitTactic.v
549
log
plain
-rw-r--r--
Inductive.v
1427
log
plain
-rw-r--r--
Injection.v
1769
log
plain
-rw-r--r--
Inversion.v
2859
log
plain
-rw-r--r--
LegacyField.v
1768
log
plain
-rw-r--r--
LetIn.v
356
log
plain
-rw-r--r--
LetPat.v
1756
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
125
log
plain
-rw-r--r--
Notations.v
1077
log
plain
-rw-r--r--
Omega.v
2197
log
plain
-rw-r--r--
Omega0.v
2449
log
plain
-rw-r--r--
Omega2.v
764
log
plain
-rw-r--r--
OmegaPre.v
2183
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
2243
log
plain
-rw-r--r--
ROmega0.v
2564
log
plain
-rw-r--r--
ROmega2.v
984
log
plain
-rw-r--r--
ROmegaPre.v
2204
log
plain
-rw-r--r--
RecTutorial.v
25255
log
plain
-rw-r--r--
Record.v
2253
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--
Reordering.v
378
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--
apply.v
6323
log
plain
-rw-r--r--
autorewritein.v
521
log
plain
-rw-r--r--
cc.v
2403
log
plain
-rw-r--r--
change.v
186
log
plain
-rw-r--r--
clear.v
291
log
plain
-rw-r--r--
coercions.v
2133
log
plain
-rw-r--r--
conv_pbs.v
7485
log
plain
-rw-r--r--
coqbugs0181.v
211
log
plain
-rw-r--r--
decl_mode.v
5547
log
plain
-rw-r--r--
dependentind.v
3330
log
plain
-rw-r--r--
destruct.v
1089
log
plain
-rw-r--r--
eauto.v
1868
log
plain
-rw-r--r--
eqdecide.v
912
log
plain
-rw-r--r--
evars.v
6522
log
plain
-rw-r--r--
extraction.v
14264
log
plain
-rw-r--r--
fix.v
2212
log
plain
-rw-r--r--
guard.v
322
log
plain
-rw-r--r--
hyps_inclusion.v
1153
log
plain
-rw-r--r--
if.v
366
log
plain
-rw-r--r--
implicit.v
1117
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--
instantiate.v
292
log
plain
-rw-r--r--
intros.v
168
log
plain
-rw-r--r--
ltac.v
4393
log
plain
-rw-r--r--
mutual_ind.v
1604
log
plain
-rw-r--r--
options.v
690
log
plain
-rw-r--r--
params_ind.v
93
log
plain
-rw-r--r--
parsing.v
243
log
plain
-rw-r--r--
pattern.v
379
log
plain
-rw-r--r--
polymorphism.v
220
log
plain
-rw-r--r--
refine.v
2668
log
plain
-rw-r--r--
replace.v
359
log
plain
-rw-r--r--
rewrite.v
944
log
plain
-rw-r--r--
rewrite_in.v
148
log
plain
-rw-r--r--
rewrite_iterated.v
545
log
plain
-rw-r--r--
set.v
90
log
plain
-rw-r--r--
setoid_ring_module.v
925
log
plain
-rw-r--r--
setoid_test.v
2657
log
plain
-rw-r--r--
setoid_test2.v
8257
log
plain
-rw-r--r--
setoid_test_function_space.v
1434
log
plain
-rw-r--r--
simpl.v
1239
log
plain
-rw-r--r--
specialize.v
1459
log
plain
-rw-r--r--
unfold.v
644
log
plain
-rw-r--r--
unicode_utf8.v
2172
log
plain
-rw-r--r--
unification.v
3912
log
plain
-rw-r--r--
univers.v
1752
log
plain