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
445
log
plain
-rw-r--r--
AdvancedCanonicalStructure.v
2844
log
plain
-rw-r--r--
AdvancedTypeClasses.v
2253
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
2072
log
plain
-rw-r--r--
Case13.v
2149
log
plain
-rw-r--r--
Case14.v
510
log
plain
-rw-r--r--
Case15.v
1315
log
plain
-rw-r--r--
Case16.v
405
log
plain
-rw-r--r--
Case17.v
1844
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--
Case3.v
720
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
2598
log
plain
-rw-r--r--
Cases-bug1834.v
379
log
plain
-rw-r--r--
Cases.v
38683
log
plain
-rw-r--r--
CasesDep.v
14500
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
644
log
plain
-rw-r--r--
Field.v
1978
log
plain
-rw-r--r--
Fixpoint.v
2343
log
plain
-rw-r--r--
Fourier.v
281
log
plain
-rw-r--r--
Funind.v
10039
log
plain
-rw-r--r--
Generalization.v
282
log
plain
-rw-r--r--
Generalize.v
176
log
plain
-rw-r--r--
Hints.v
1577
log
plain
-rw-r--r--
ImplicitArguments.v
545
log
plain
-rw-r--r--
ImplicitTactic.v
549
log
plain
-rw-r--r--
Import.v
218
log
plain
-rw-r--r--
Inductive.v
2966
log
plain
-rw-r--r--
Injection.v
1768
log
plain
-rw-r--r--
Inversion.v
3709
log
plain
-rw-r--r--
LegacyField.v
1706
log
plain
-rw-r--r--
LetIn.v
356
log
plain
-rw-r--r--
LetPat.v
1750
log
plain
-rw-r--r--
MatchFail.v
832
log
plain
-rw-r--r--
Mod_ltac.v
302
log
plain
-rw-r--r--
Mod_params.v
1375
log
plain
-rw-r--r--
Mod_strengthen.v
963
log
plain
-rw-r--r--
Mod_type.v
519
log
plain
-rw-r--r--
NatRing.v
125
log
plain
-rw-r--r--
Notations.v
3155
log
plain
-rw-r--r--
Nsatz.v
14259
log
plain
-rw-r--r--
Omega.v
2197
log
plain
-rw-r--r--
Omega0.v
2427
log
plain
-rw-r--r--
Omega2.v
763
log
plain
-rw-r--r--
OmegaPre.v
2195
log
plain
-rw-r--r--
PCase.v
1515
log
plain
-rw-r--r--
PPFix.v
207
log
plain
-rw-r--r--
Print.v
282
log
plain
-rw-r--r--
PrintSortedUniverses.v
39
log
plain
-rw-r--r--
ProgramWf.v
2271
log
plain
-rw-r--r--
Projection.v
1151
log
plain
-rw-r--r--
ROmega.v
2242
log
plain
-rw-r--r--
ROmega0.v
2542
log
plain
-rw-r--r--
ROmega2.v
982
log
plain
-rw-r--r--
ROmegaPre.v
2216
log
plain
-rw-r--r--
RecTutorial.v
25146
log
plain
-rw-r--r--
Record.v
2399
log
plain
-rw-r--r--
Reg.v
3062
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--
Scheme.v
82
log
plain
-rw-r--r--
Scopes.v
158
log
plain
-rw-r--r--
Section.v
136
log
plain
-rw-r--r--
Simplify_eq.v
252
log
plain
-rw-r--r--
Tauto.v
5145
log
plain
-rw-r--r--
TestRefine.v
4315
log
plain
-rw-r--r--
Try.v
174
log
plain
-rw-r--r--
Typeclasses.v
1458
log
plain
-rw-r--r--
apply.v
11002
log
plain
-rw-r--r--
auto.v
548
log
plain
-rw-r--r--
autointros.v
462
log
plain
-rw-r--r--
autorewrite.v
763
log
plain
-rw-r--r--
bullet.v
53
log
plain
-rw-r--r--
cc.v
2331
log
plain
-rw-r--r--
change.v
1081
log
plain
-rw-r--r--
clear.v
290
log
plain
-rw-r--r--
coercions.v
3757
log
plain
-rw-r--r--
conv_pbs.v
7579
log
plain
-rw-r--r--
coqbugs0181.v
211
log
plain
-rw-r--r--
decl_mode.v
5537
log
plain
-rw-r--r--
dependentind.v
3932
log
plain
-rw-r--r--
destruct.v
1910
log
plain
-rw-r--r--
eauto.v
1867
log
plain
-rw-r--r--
eqdecide.v
819
log
plain
-rw-r--r--
eta.v
595
log
plain
-rw-r--r--
evars.v
12128
log
plain
-rw-r--r--
extraction.v
14186
log
plain
-rw-r--r--
fix.v
2168
log
plain
-rw-r--r--
guard.v
322
log
plain
-rw-r--r--
hyps_inclusion.v
1160
log
plain
-rw-r--r--
if.v
366
log
plain
-rw-r--r--
implicit.v
2761
log
plain
-rw-r--r--
import_lib.v
3415
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
1783
log
plain
-rw-r--r--
instantiate.v
292
log
plain
-rw-r--r--
intros.v
168
log
plain
-rw-r--r--
ltac.v
6227
log
plain
-rw-r--r--
mutual_ind.v
1601
log
plain
-rw-r--r--
options.v
690
log
plain
-rw-r--r--
params_ind.v
93
log
plain
-rw-r--r--
parsing.v
218
log
plain
-rw-r--r--
pattern.v
1400
log
plain
-rw-r--r--
polymorphism.v
219
log
plain
-rw-r--r--
proof_using.v
708
log
plain
-rw-r--r--
refine.v
2661
log
plain
-rw-r--r--
remember.v
225
log
plain
-rw-r--r--
replace.v
635
log
plain
-rw-r--r--
rewrite.v
3306
log
plain
-rw-r--r--
rewrite_in.v
148
log
plain
-rw-r--r--
rewrite_iterated.v
545
log
plain
-rw-r--r--
searchabout.v
1690
log
plain
-rw-r--r--
set.v
90
log
plain
-rw-r--r--
setoid_ring_module.v
922
log
plain
-rw-r--r--
setoid_test.v
3894
log
plain
-rw-r--r--
setoid_test2.v
8251
log
plain
-rw-r--r--
setoid_test_function_space.v
1117
log
plain
-rw-r--r--
simpl.v
1232
log
plain
-rw-r--r--
simpl_tuning.v
3895
log
plain
-rw-r--r--
specialize.v
1416
log
plain
-rw-r--r--
telescope_canonical.v
2393
log
plain
-rw-r--r--
unfold.v
812
log
plain
-rw-r--r--
unicode_utf8.v
2173
log
plain
-rw-r--r--
unification.v
5809
log
plain
-rw-r--r--
univers.v
1575
log
plain
-rw-r--r--
universes-coercion.v
917
log
plain