index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
output
Mode
Name
Size
-rw-r--r--
Arguments.out
3458
log
plain
-rw-r--r--
Arguments.v
1468
log
plain
-rw-r--r--
ArgumentsScope.out
1083
log
plain
-rw-r--r--
ArgumentsScope.v
535
log
plain
-rw-r--r--
Arguments_renaming.out
4147
log
plain
-rw-r--r--
Arguments_renaming.v
1018
log
plain
-rw-r--r--
Cases.out
1542
log
plain
-rw-r--r--
Cases.v
1607
log
plain
-rw-r--r--
Coercions.out
108
log
plain
-rw-r--r--
Coercions.v
651
log
plain
-rw-r--r--
Errors.out
296
log
plain
-rw-r--r--
Errors.v
359
log
plain
-rw-r--r--
Existentials.out
234
log
plain
-rw-r--r--
Existentials.v
225
log
plain
-rw-r--r--
Extraction_matchs_2413.out
1058
log
plain
-rw-r--r--
Extraction_matchs_2413.v
2742
log
plain
-rw-r--r--
Fixpoint.out
463
log
plain
-rw-r--r--
Fixpoint.v
1048
log
plain
-rw-r--r--
Implicit.out
391
log
plain
-rw-r--r--
Implicit.v
1267
log
plain
-rw-r--r--
InitSyntax.out
393
log
plain
-rw-r--r--
InitSyntax.v
111
log
plain
-rw-r--r--
Intuition.out
86
log
plain
-rw-r--r--
Intuition.v
121
log
plain
-rw-r--r--
Match_subterm.out
36
log
plain
-rw-r--r--
Match_subterm.v
86
log
plain
-rw-r--r--
Nametab.out
1672
log
plain
-rw-r--r--
Nametab.v
917
log
plain
-rw-r--r--
Naming.out
1659
log
plain
-rw-r--r--
Naming.v
1957
log
plain
-rw-r--r--
Notations.out
3672
log
plain
-rw-r--r--
Notations.v
8518
log
plain
-rw-r--r--
Notations2.out
1199
log
plain
-rw-r--r--
Notations2.v
3163
log
plain
-rw-r--r--
NumbersSyntax.out
950
log
plain
-rw-r--r--
NumbersSyntax.v
1351
log
plain
-rw-r--r--
PrintAssumptions.out
574
log
plain
-rw-r--r--
PrintAssumptions.v
2582
log
plain
-rw-r--r--
PrintInfos.out
4356
log
plain
-rw-r--r--
PrintInfos.v
1169
log
plain
-rw-r--r--
PrintModule.out
82
log
plain
-rw-r--r--
PrintModule.v
369
log
plain
-rw-r--r--
Quote.out
972
log
plain
-rw-r--r--
Quote.v
911
log
plain
-rw-r--r--
RealSyntax.out
31
log
plain
-rw-r--r--
RealSyntax.v
49
log
plain
-rw-r--r--
Record.out
212
log
plain
-rw-r--r--
Record.v
385
log
plain
-rw-r--r--
Search.out
4123
log
plain
-rw-r--r--
Search.v
1122
log
plain
-rw-r--r--
SearchHead.out
1411
log
plain
-rw-r--r--
SearchHead.v
460
log
plain
-rw-r--r--
SearchPattern.out
2217
log
plain
-rw-r--r--
SearchPattern.v
1002
log
plain
-rw-r--r--
SearchRewrite.out
120
log
plain
-rw-r--r--
SearchRewrite.v
384
log
plain
-rw-r--r--
Sum.out
99
log
plain
-rw-r--r--
Sum.v
93
log
plain
-rw-r--r--
Tactics.out
128
log
plain
-rw-r--r--
Tactics.v
357
log
plain
-rw-r--r--
TranspModtype.out
89
log
plain
-rw-r--r--
TranspModtype.v
385
log
plain
-rw-r--r--
ZSyntax.out
578
log
plain
-rw-r--r--
ZSyntax.v
558
log
plain
-rw-r--r--
inference.out
561
log
plain
-rw-r--r--
inference.v
856
log
plain
-rw-r--r--
ltac.out
141
log
plain
-rw-r--r--
ltac.v
422
log
plain
-rw-r--r--
names.out
168
log
plain
-rw-r--r--
names.v
132
log
plain
-rw-r--r--
reduction.out
44
log
plain
-rw-r--r--
reduction.v
279
log
plain
-rw-r--r--
rewrite-2172.out
91
log
plain
-rw-r--r--
rewrite-2172.v
734
log
plain
-rw-r--r--
set.out
279
log
plain
-rw-r--r--
set.v
154
log
plain
-rw-r--r--
simpl.out
201
log
plain
-rw-r--r--
simpl.v
148
log
plain