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--
ArgumentsScope.out
1083
log
plain
-rw-r--r--
ArgumentsScope.v
535
log
plain
-rw-r--r--
Cases.out
916
log
plain
-rw-r--r--
Cases.v
839
log
plain
-rw-r--r--
Coercions.out
90
log
plain
-rw-r--r--
Coercions.v
413
log
plain
-rw-r--r--
Existentials.out
48
log
plain
-rw-r--r--
Existentials.v
225
log
plain
-rw-r--r--
Fixpoint.out
612
log
plain
-rw-r--r--
Fixpoint.v
898
log
plain
-rw-r--r--
Implicit.out
344
log
plain
-rw-r--r--
Implicit.v
947
log
plain
-rw-r--r--
InitSyntax.out
382
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
1114
log
plain
-rw-r--r--
Nametab.v
917
log
plain
-rw-r--r--
Notations.out
1128
log
plain
-rw-r--r--
Notations.v
4843
log
plain
-rw-r--r--
Notations2.out
95
log
plain
-rw-r--r--
Notations2.v
434
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--
Sum.out
99
log
plain
-rw-r--r--
Sum.v
93
log
plain
-rw-r--r--
Tactics.out
132
log
plain
-rw-r--r--
Tactics.v
488
log
plain
-rw-r--r--
TranspModtype.out
89
log
plain
-rw-r--r--
TranspModtype.v
385
log
plain
-rw-r--r--
ZSyntax.out
571
log
plain
-rw-r--r--
ZSyntax.v
558
log
plain
-rw-r--r--
reduction.out
44
log
plain
-rw-r--r--
reduction.v
278
log
plain
-rw-r--r--
set.out
315
log
plain
-rw-r--r--
set.v
154
log
plain
