index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
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
3365
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
349
log
plain
-rw-r--r--
Case12.v
2083
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
409
log
plain
-rw-r--r--
Case17.v
1860
log
plain
-rw-r--r--
Case18.v
513
log
plain
-rw-r--r--
Case19.v
542
log
plain
-rw-r--r--
Case2.v
306
log
plain
-rw-r--r--
Case20.v
1106
log
plain
-rw-r--r--
Case21.v
476
log
plain
-rw-r--r--
Case22.v
1756
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
478
log
plain
-rw-r--r--
Case8.v
338
log
plain
-rw-r--r--
Case9.v
2269
log
plain
-rw-r--r--
CaseAlias.v
2598
log
plain
-rw-r--r--
CaseInClause.v
659
log
plain
-rw-r--r--
Cases-bug1834.v
383
log
plain
-rw-r--r--
Cases-bug3758.v
386
log
plain
-rw-r--r--
Cases.v
39353
log
plain
-rw-r--r--
CasesDep.v
14537
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
2347
log
plain
-rw-r--r--
Fourier.v
281
log
plain
-rw-r--r--
Funind.v
10145
log
plain
-rw-r--r--
Generalization.v
282
log
plain
-rw-r--r--
Generalize.v
176
log
plain
-rw-r--r--
Hints.v
2885
log
plain
-rw-r--r--
ImplicitArguments.v
627
log
plain
-rw-r--r--
ImplicitTactic.v
549
log
plain
-rw-r--r--
Import.v
218
log
plain
-rw-r--r--
Inductive.v
5058
log
plain
-rw-r--r--
Injection.v
3232
log
plain
-rw-r--r--
Inversion.v
5372
log
plain
-rw-r--r--
LetIn.v
356
log
plain
-rw-r--r--
LetPat.v
1760
log
plain
-rw-r--r--
MatchFail.v
844
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
3381
log
plain
-rw-r--r--
Notations2.v
4650
log
plain
-rw-r--r--
Nsatz.v
14291
log
plain
-rw-r--r--
NumberScopes.v
1367
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
2278
log
plain
-rw-r--r--
Projection.v
1278
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
25136
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
454
log
plain
-rw-r--r--
Section.v
136
log
plain
-rw-r--r--
Simplify_eq.v
252
log
plain
-rw-r--r--
TacticNotation1.v
198
log
plain
-rw-r--r--
Tauto.v
5145
log
plain
-rw-r--r--
TestRefine.v
4320
log
plain
-rw-r--r--
Try.v
174
log
plain
-rw-r--r--
Typeclasses.v
1814
log
plain
-rw-r--r--
apply.v
14153
log
plain
-rw-r--r--
applyTC.v
289
log
plain
-rw-r--r--
auto.v
3284
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
2878
log
plain
-rw-r--r--
change.v
1592
log
plain
-rw-r--r--
clear.v
290
log
plain
-rw-r--r--
coercions.v
3769
log
plain
-rw-r--r--
coindprim.v
1107
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
5544
log
plain
-rw-r--r--
decl_mode2.v
5234
log
plain
-rw-r--r--
dependentind.v
3932
log
plain
-rw-r--r--
destruct.v
9757
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
13248
log
plain
-rw-r--r--
extraction.v
14186
log
plain
-rw-r--r--
extraction_dep.v
857
log
plain
-rw-r--r--
extraction_impl.v
1649
log
plain
-rw-r--r--
extraction_polyprop.v
362
log
plain
-rw-r--r--
fix.v
2182
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
2763
log
plain
-rw-r--r--
import_lib.v
3415
log
plain
-rw-r--r--
import_mod.v
993
log
plain
-rw-r--r--
indelim.v
1359
log
plain
-rw-r--r--
inds_type_sec.v
594
log
plain
-rw-r--r--
induct.v
4893
log
plain
-rw-r--r--
intros.v
2910
log
plain
-rw-r--r--
keyedrewrite.v
1383
log
plain
-rw-r--r--
letproj.v
224
log
plain
-rw-r--r--
ltac.v
6617
log
plain
-rw-r--r--
ltac_plus.v
356
log
plain
-rw-r--r--
mutual_ind.v
1601
log
plain
-rw-r--r--
namedunivs.v
2799
log
plain
-rw-r--r--
options.v
690
log
plain
-rw-r--r--
paralleltac.v
975
log
plain
-rw-r--r--
parsing.v
218
log
plain
-rw-r--r--
pattern.v
1400
log
plain
-rw-r--r--
polymorphism.v
7420
log
plain
-rw-r--r--
primitiveproj.v
4481
log
plain
-rw-r--r--
proof_using.v
2575
log
plain
-rw-r--r--
qed_export.v
323
log
plain
-rw-r--r--
record_syntax.v
802
log
plain
-rw-r--r--
refine.v
2672
log
plain
-rw-r--r--
remember.v
409
log
plain
-rw-r--r--
replace.v
635
log
plain
-rw-r--r--
rewrite.v
3931
log
plain
-rw-r--r--
rewrite_dep.v
929
log
plain
-rw-r--r--
rewrite_in.v
148
log
plain
-rw-r--r--
rewrite_iterated.v
545
log
plain
-rw-r--r--
rewrite_strat.v
1274
log
plain
-rw-r--r--
searchabout.v
1690
log
plain
-rw-r--r--
set.v
408
log
plain
-rw-r--r--
setoid_ring_module.v
922
log
plain
-rw-r--r--
setoid_test.v
3948
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--
setoid_unif.v
911
log
plain
-rw-r--r--
shrink_abstract.v
220
log
plain
-rw-r--r--
shrink_obligations.v
605
log
plain
-rw-r--r--
sideff.v
277
log
plain
-rw-r--r--
simpl.v
2695
log
plain
-rw-r--r--
simpl_tuning.v
3895
log
plain
-rw-r--r--
somatching.v
1534
log
plain
-rw-r--r--
specialize.v
1960
log
plain
-rw-r--r--
subst.v
591
log
plain
-rw-r--r--
telescope_canonical.v
2393
log
plain
-rw-r--r--
tryif.v
1331
log
plain
-rw-r--r--
unfold.v
812
log
plain
-rw-r--r--
unicode_utf8.v
2216
log
plain
-rw-r--r--
unification.v
5958
log
plain
-rw-r--r--
univers.v
1964
log
plain
-rw-r--r--
universes-coercion.v
917
log
plain
-rw-r--r--
univnames.v
733
log
plain
-rw-r--r--
univscompute.v
721
log
plain
-rw-r--r--
unshelve.v
216
log
plain
-rw-r--r--
vm_univ_poly.v
4212
log
plain
-rw-r--r--
vm_univ_poly_match.v
606
log
plain