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
3896
log
plain
-rw-r--r--
Arguments.v
1468
log
plain
-rw-r--r--
ArgumentsScope.out
1539
log
plain
-rw-r--r--
ArgumentsScope.v
535
log
plain
-rw-r--r--
Arguments_renaming.out
4410
log
plain
-rw-r--r--
Arguments_renaming.v
1018
log
plain
-rw-r--r--
Cases.out
1509
log
plain
-rw-r--r--
Cases.v
1400
log
plain
-rw-r--r--
Coercions.out
108
log
plain
-rw-r--r--
Coercions.v
651
log
plain
-rw-r--r--
Errors.out
326
log
plain
-rw-r--r--
Errors.v
359
log
plain
-rw-r--r--
Existentials.out
238
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
422
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
91
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
1815
log
plain
-rw-r--r--
Naming.v
1957
log
plain
-rw-r--r--
Notations.out
3956
log
plain
-rw-r--r--
Notations.v
8472
log
plain
-rw-r--r--
Notations2.out
1261
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
844
log
plain
-rw-r--r--
PrintAssumptions.v
2422
log
plain
-rw-r--r--
PrintInfos.out
4472
log
plain
-rw-r--r--
PrintInfos.v
682
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
1392
log
plain
-rw-r--r--
Search.v
155
log
plain
-rw-r--r--
SearchPattern.out
2272
log
plain
-rw-r--r--
SearchPattern.v
408
log
plain
-rw-r--r--
SearchRewrite.out
72
log
plain
-rw-r--r--
SearchRewrite.v
118
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
229
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
436
log
plain
-rw-r--r--
inference.v
856
log
plain
-rw-r--r--
names.out
178
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
101
log
plain
-rw-r--r--
rewrite-2172.v
734
log
plain
-rw-r--r--
set.out
315
log
plain
-rw-r--r--
set.v
154
log
plain
-rw-r--r--
simpl.out
201
log
plain
-rw-r--r--
simpl.v
154
log
plain