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--
.cvsignore
5
log
plain
-rw-r--r--
Case1.v
400
log
plain
-rw-r--r--
Case10.v
764
log
plain
-rw-r--r--
Case11.v
285
log
plain
-rw-r--r--
Case12.v
1442
log
plain
-rw-r--r--
Case13.v
959
log
plain
-rw-r--r--
Case14.v
489
log
plain
-rw-r--r--
Case2.v
339
log
plain
-rw-r--r--
Case5.v
351
log
plain
-rw-r--r--
Case6.v
597
log
plain
-rw-r--r--
Case7.v
459
log
plain
-rw-r--r--
Case9.v
2270
log
plain
-rw-r--r--
CaseAlias.v
380
log
plain
-rw-r--r--
Cases.v
46156
log
plain
-rw-r--r--
CasesDep.v
10635
log
plain
-rw-r--r--
Check.v
788
log
plain
-rw-r--r--
Conjecture.v
210
log
plain
-rw-r--r--
DHyp.v
205
log
plain
-rw-r--r--
Decompose.v
187
log
plain
-rw-r--r--
Destruct.v
236
log
plain
-rw-r--r--
DiscrR.v
395
log
plain
-rw-r--r--
Discriminate.v
196
log
plain
-rw-r--r--
Field.v
1437
log
plain
-rw-r--r--
Fourier.v
300
log
plain
-rw-r--r--
Funind.v
9921
log
plain
-rw-r--r--
Generalize.v
137
log
plain
-rw-r--r--
Hints.v
1559
log
plain
-rw-r--r--
Inductive.v
1057
log
plain
-rw-r--r--
Injection.v
814
log
plain
-rw-r--r--
Inversion.v
488
log
plain
-rw-r--r--
LetIn.v
314
log
plain
-rw-r--r--
MatchFail.v
958
log
plain
-rw-r--r--
Mod_ltac.v
264
log
plain
-rw-r--r--
Mod_params.v
1325
log
plain
-rw-r--r--
Mod_strengthen.v
889
log
plain
-rw-r--r--
NatRing.v
144
log
plain
-rw-r--r--
Omega.v
1512
log
plain
-rw-r--r--
Print.v
297
log
plain
-rw-r--r--
Projection.v
1059
log
plain
-rw-r--r--
Record.v
105
log
plain
-rw-r--r--
Reg.v
2837
log
plain
-rw-r--r--
Remark.v
172
log
plain
-rw-r--r--
Rename.v
78
log
plain
-rw-r--r--
Require.v
85
log
plain
-rw-r--r--
Simplify_eq.v
241
log
plain
-rw-r--r--
Tauto.v
4770
log
plain
-rw-r--r--
Try.v
176
log
plain
-rw-r--r--
cc.v
1721
log
plain
-rw-r--r--
coercions.v
202
log
plain
-rw-r--r--
coqbugs0181.v
202
log
plain
-rw-r--r--
eauto.v
1262
log
plain
-rw-r--r--
eqdecide.v
831
log
plain
-rw-r--r--
evars.v
802
log
plain
-rw-r--r--
fix.v
1654
log
plain
-rw-r--r--
if.v
154
log
plain
-rw-r--r--
implicit.v
465
log
plain
-rw-r--r--
import_lib.v
3548
log
plain
-rw-r--r--
import_mod.v
981
log
plain
-rw-r--r--
inds_type_sec.v
583
log
plain
-rw-r--r--
induct.v
686
log
plain
-rw-r--r--
ltac.v
1512
log
plain
-rw-r--r--
mutual_ind.v
1508
log
plain
-rw-r--r--
options.v
662
log
plain
-rw-r--r--
refine.v
498
log
plain
-rw-r--r--
setoid_test.v
1708
log
plain
-rw-r--r--
unfold.v
641
log
plain
-rw-r--r--
univers.v
305
log
plain