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--
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
46153
log
plain
-rw-r--r--
CasesDep.v
10699
log
plain
-rw-r--r--
Check.v
788
log
plain
-rw-r--r--
DHyp.v
205
log
plain
-rw-r--r--
Decompose.v
187
log
plain
-rw-r--r--
Destruct.v
195
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
301
log
plain
-rw-r--r--
Hints.v
1559
log
plain
-rw-r--r--
Injection.v
254
log
plain
-rw-r--r--
LetIn.v
314
log
plain
-rw-r--r--
MatchFail.v
958
log
plain
-rw-r--r--
Mod_params.v
1325
log
plain
-rw-r--r--
NatRing.v
144
log
plain
-rw-r--r--
Omega.v
982
log
plain
-rw-r--r--
Print.v
297
log
plain
-rw-r--r--
Reg.v
2901
log
plain
-rw-r--r--
Remark.v
122
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--
cc.v
962
log
plain
-rw-r--r--
coercions.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
1319
log
plain
-rw-r--r--
fix.v
1654
log
plain
-rw-r--r--
if.v
154
log
plain
-rw-r--r--
implicit.v
434
log
plain
-rw-r--r--
inds_type_sec.v
582
log
plain
-rw-r--r--
induct.v
686
log
plain
-rw-r--r--
ltac.v
484
log
plain
-rw-r--r--
mutual_ind.v
1508
log
plain
-rw-r--r--
options.v
662
log
plain
-rw-r--r--
refine.v
282
log
plain
-rw-r--r--
setoid_test.v
1708
log
plain
-rw-r--r--
unfold.v
641
log
plain
-rw-r--r--
univers.v
273
log
plain