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
3329
log
plain
-rw-r--r--
Arguments.v
1383
log
plain
-rw-r--r--
ArgumentsScope.out
1393
log
plain
-rw-r--r--
ArgumentsScope.v
535
log
plain
-rw-r--r--
Arguments_renaming.out
3970
log
plain
-rw-r--r--
Arguments_renaming.v
992
log
plain
-rw-r--r--
Cases.out
1113
log
plain
-rw-r--r--
Cases.v
1066
log
plain
-rw-r--r--
Coercions.out
108
log
plain
-rw-r--r--
Coercions.v
651
log
plain
-rw-r--r--
Errors.out
87
log
plain
-rw-r--r--
Errors.v
174
log
plain
-rw-r--r--
Existentials.out
185
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
2732
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
389
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
25
log
plain
-rw-r--r--
Match_subterm.v
86
log
plain
-rw-r--r--
Nametab.out
1149
log
plain
-rw-r--r--
Nametab.v
917
log
plain
-rw-r--r--
Naming.out
1789
log
plain
-rw-r--r--
Naming.v
1957
log
plain
-rw-r--r--
Notations.out
3533
log
plain
-rw-r--r--
Notations.v
7831
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
552
log
plain
-rw-r--r--
PrintAssumptions.v
2422
log
plain
-rw-r--r--
PrintInfos.out
4287
log
plain
-rw-r--r--
PrintInfos.v
673
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
896
log
plain
-rw-r--r--
Search.v
143
log
plain
-rw-r--r--
SearchPattern.out
791
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
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
166
log
plain
-rw-r--r--
inference.v
272
log
plain
-rw-r--r--
names.out
188
log
plain
-rw-r--r--
names.v
132
log
plain
-rw-r--r--
reduction.out
44
log
plain
-rw-r--r--
reduction.v
278
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
148
log
plain