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
438
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
2476
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
970
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
2646
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
984
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
39497
log
plain
-rw-r--r--
CasesDep.v
14537
log
plain
-rw-r--r--
Check.v
814
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
822
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
10180
log
plain
-rw-r--r--
FunindExtraction_compat86.v
10204
log
plain
-rw-r--r--
Generalization.v
282
log
plain
-rw-r--r--
Generalize.v
176
log
plain
-rw-r--r--
Hints.v
4986
log
plain
-rw-r--r--
ImplicitArguments.v
1045
log
plain
-rw-r--r--
ImplicitTactic.v
549
log
plain
-rw-r--r--
Import.v
218
log
plain
-rw-r--r--
Inductive.v
5906
log
plain
-rw-r--r--
Injection.v
4023
log
plain
-rw-r--r--
Inversion.v
5361
log
plain
-rw-r--r--
InversionSigma.v
1574
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
515
log
plain
-rw-r--r--
NatRing.v
125
log
plain
-rw-r--r--
Notations.v
4808
log
plain
-rw-r--r--
Notations2.v
5302
log
plain
-rw-r--r--
Nsatz.v
14291
log
plain
-rw-r--r--
NumberScopes.v
921
log
plain
-rw-r--r--
Omega.v
2193
log
plain
-rw-r--r--
Omega0.v
2429
log
plain
-rw-r--r--
Omega2.v
765
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--
PatternsInBinders.v
1426
log
plain
-rw-r--r--
Print.v
282
log
plain
-rw-r--r--
PrintSortedUniverses.v
39
log
plain
-rw-r--r--
ProgramWf.v
2279
log
plain
-rw-r--r--
Projection.v
1278
log
plain
-rw-r--r--
ROmega.v
2238
log
plain
-rw-r--r--
ROmega0.v
2757
log
plain
-rw-r--r--
ROmega2.v
984
log
plain
-rw-r--r--
ROmega3.v
872
log
plain
-rw-r--r--
ROmega4.v
488
log
plain
-rw-r--r--
ROmegaPre.v
2216
log
plain
-rw-r--r--
RecTutorial.v
25156
log
plain
-rw-r--r--
Record.v
2592
log
plain
-rw-r--r--
Reg.v
3062
log
plain
-rw-r--r--
Remark.v
172
log
plain
-rw-r--r--
Rename.v
222
log
plain
-rw-r--r--
Reordering.v
378
log
plain
-rw-r--r--
Require.v
88
log
plain
-rw-r--r--
Scheme.v
593
log
plain
-rw-r--r--
Scopes.v
552
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--
TacticNotation2.v
310
log
plain
-rw-r--r--
Tauto.v
5145
log
plain
-rw-r--r--
TestRefine.v
4315
log
plain
-rw-r--r--
Try.v
172
log
plain
-rw-r--r--
Typeclasses.v
6722
log
plain
-rw-r--r--
abstract_chain.v
885
log
plain
-rw-r--r--
abstract_poly.v
517
log
plain
-rw-r--r--
all-check.v
36
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--
boundvars.v
621
log
plain
-rw-r--r--
bteauto.v
4062
log
plain
-rw-r--r--
bullet.v
53
log
plain
-rw-r--r--
cbn.v
317
log
plain
-rw-r--r--
cc.v
3140
log
plain
-rw-r--r--
change.v
1853
log
plain
-rw-r--r--
change_pattern.v
1244
log
plain
-rw-r--r--
clear.v
568
log
plain
-rw-r--r--
coercions.v
3770
log
plain
-rw-r--r--
coindprim.v
2826
log
plain
-rw-r--r--
contradiction.v
563
log
plain
-rw-r--r--
conv_pbs.v
7579
log
plain
-rw-r--r--
coqbugs0181.v
211
log
plain
-rw-r--r--
cumulativity.v
2080
log
plain
-rw-r--r--
dependentind.v
3930
log
plain
-rw-r--r--
destruct.v
9881
log
plain
-rw-r--r--
eauto.v
5640
log
plain
-rw-r--r--
eqdecide.v
1038
log
plain
-rw-r--r--
eta.v
595
log
plain
-rw-r--r--
evars.v
13415
log
plain
-rw-r--r--
extraction.v
15015
log
plain
-rw-r--r--
extraction_dep.v
991
log
plain
-rw-r--r--
extraction_impl.v
1922
log
plain
-rw-r--r--
extraction_polyprop.v
398
log
plain
-rw-r--r--
fix.v
2182
log
plain
-rw-r--r--
forward.v
664
log
plain
-rw-r--r--
goal_selector.v
1207
log
plain
-rw-r--r--
guard.v
828
log
plain
-rw-r--r--
hintdb_in_ltac.v
275
log
plain
-rw-r--r--
hintdb_in_ltac_bis.v
237
log
plain
-rw-r--r--
hyps_inclusion.v
1160
log
plain
-rw-r--r--
if.v
365
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
1360
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
2908
log
plain
-rw-r--r--
keyedrewrite.v
1384
log
plain
-rw-r--r--
letproj.v
224
log
plain
-rw-r--r--
ltac.v
7320
log
plain
-rw-r--r--
ltac_match_pattern_names.v
604
log
plain
-rw-r--r--
ltac_plus.v
357
log
plain
-rw-r--r--
ltacprof.v
223
log
plain
-rw-r--r--
mutual_ind.v
1601
log
plain
-rw-r--r--
namedunivs.v
2799
log
plain
-rw-r--r--
old_typeclass.v
298
log
plain
-rw-r--r--
onlyprinting.v
150
log
plain
-rw-r--r--
options.v
690
log
plain
-rw-r--r--
par_abstract.v
469
log
plain
-rw-r--r--
paralleltac.v
1193
log
plain
-rw-r--r--
parsing.v
218
log
plain
-rw-r--r--
pattern.v
1400
log
plain
-rw-r--r--
polymorphism.v
11008
log
plain
-rw-r--r--
primitiveproj.v
4660
log
plain
-rw-r--r--
programequality.v
267
log
plain
-rw-r--r--
proof_using.v
2575
log
plain
-rw-r--r--
record_syntax.v
920
log
plain
-rw-r--r--
refine.v
2971
log
plain
-rw-r--r--
remember.v
626
log
plain
-rw-r--r--
replace.v
635
log
plain
-rw-r--r--
rewrite.v
3931
log
plain
-rw-r--r--
rewrite_dep.v
930
log
plain
-rw-r--r--
rewrite_evar.v
376
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
1275
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
4488
log
plain
-rw-r--r--
setoid_test2.v
8535
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
2693
log
plain
-rw-r--r--
simpl_tuning.v
3897
log
plain
-rw-r--r--
somatching.v
1534
log
plain
-rw-r--r--
specialize.v
3465
log
plain
-rw-r--r--
ssrpattern.v
514
log
plain
-rw-r--r--
subst.v
984
log
plain
-rw-r--r--
telescope_canonical.v
2393
log
plain
-rw-r--r--
transparent_abstract.v
800
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--
unidecls.v
2228
log
plain
-rw-r--r--
unification.v
6301
log
plain
-rw-r--r--
univers.v
1943
log
plain
-rw-r--r--
universes-coercion.v
917
log
plain
-rw-r--r--
univnames.v
904
log
plain
-rw-r--r--
univscompute.v
721
log
plain
-rw-r--r--
unshelve.v
401
log
plain
-rw-r--r--
vm_univ_poly.v
4178
log
plain
-rw-r--r--
vm_univ_poly_match.v
606
log
plain