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
3449
log
plain
-rw-r--r--
Arguments.v
1470
log
plain
-rw-r--r--
ArgumentsScope.out
1083
log
plain
-rw-r--r--
ArgumentsScope.v
560
log
plain
-rw-r--r--
Arguments_renaming.out
4329
log
plain
-rw-r--r--
Arguments_renaming.v
1049
log
plain
-rw-r--r--
Binder.out
168
log
plain
-rw-r--r--
Binder.v
134
log
plain
-rw-r--r--
Cases.out
4548
log
plain
-rw-r--r--
Cases.v
6316
log
plain
-rw-r--r--
Coercions.out
108
log
plain
-rw-r--r--
Coercions.v
651
log
plain
-rw-r--r--
CompactContexts.out
142
log
plain
-rw-r--r--
CompactContexts.v
141
log
plain
-rw-r--r--
ErrorInModule.out
116
log
plain
-rw-r--r--
ErrorInModule.v
101
log
plain
-rw-r--r--
ErrorInSection.out
116
log
plain
-rw-r--r--
ErrorInSection.v
102
log
plain
-rw-r--r--
Errors.out
451
log
plain
-rw-r--r--
Errors.v
548
log
plain
-rw-r--r--
Existentials.out
237
log
plain
-rw-r--r--
Existentials.v
225
log
plain
-rw-r--r--
Extraction_infix.out
279
log
plain
-rw-r--r--
Extraction_infix.v
623
log
plain
-rw-r--r--
Extraction_matchs_2413.out
1058
log
plain
-rw-r--r--
Extraction_matchs_2413.v
2778
log
plain
-rw-r--r--
Fixpoint.out
519
log
plain
-rw-r--r--
Fixpoint.v
1177
log
plain
-rw-r--r--
FunExt.out
866
log
plain
-rw-r--r--
FunExt.v
4767
log
plain
-rw-r--r--
Implicit.out
391
log
plain
-rw-r--r--
Implicit.v
1265
log
plain
-rw-r--r--
Inductive.out
143
log
plain
-rw-r--r--
Inductive.v
94
log
plain
-rw-r--r--
InitSyntax.out
433
log
plain
-rw-r--r--
InitSyntax.v
111
log
plain
-rw-r--r--
Int31Syntax.out
154
log
plain
-rw-r--r--
Int31Syntax.v
431
log
plain
-rw-r--r--
Intuition.out
85
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
1639
log
plain
-rw-r--r--
Naming.v
1957
log
plain
-rw-r--r--
Notations.out
3619
log
plain
-rw-r--r--
Notations.v
8889
log
plain
-rw-r--r--
Notations2.out
2017
log
plain
-rw-r--r--
Notations2.v
4899
log
plain
-rw-r--r--
Notations3.out
4438
log
plain
-rw-r--r--
Notations3.v
8884
log
plain
-rw-r--r--
PatternsInBinders.out
1239
log
plain
-rw-r--r--
PatternsInBinders.v
1704
log
plain
-rw-r--r--
PrintAssumptions.out
574
log
plain
-rw-r--r--
PrintAssumptions.v
2582
log
plain
-rw-r--r--
PrintInfos.out
3366
log
plain
-rw-r--r--
PrintInfos.v
947
log
plain
-rw-r--r--
PrintModule.out
146
log
plain
-rw-r--r--
PrintModule.v
567
log
plain
-rw-r--r--
Quote.out
963
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--
RecognizePluginWarning.out
0
log
plain
-rw-r--r--
RecognizePluginWarning.v
289
log
plain
-rw-r--r--
Record.out
628
log
plain
-rw-r--r--
Record.v
822
log
plain
-rw-r--r--
Search.out
4430
log
plain
-rw-r--r--
Search.v
1253
log
plain
-rw-r--r--
SearchHead.out
1411
log
plain
-rw-r--r--
SearchHead.v
460
log
plain
-rw-r--r--
SearchPattern.out
2215
log
plain
-rw-r--r--
SearchPattern.v
1003
log
plain
-rw-r--r--
SearchRewrite.out
120
log
plain
-rw-r--r--
SearchRewrite.v
384
log
plain
-rw-r--r--
Show.out
148
log
plain
-rw-r--r--
Show.v
267
log
plain
-rw-r--r--
ShowMatch.out
58
log
plain
-rw-r--r--
ShowMatch.v
349
log
plain
-rw-r--r--
ShowProof.out
31
log
plain
-rw-r--r--
ShowProof.v
145
log
plain
-rw-r--r--
SuggestProofUsing.out
222
log
plain
-rw-r--r--
SuggestProofUsing.v
547
log
plain
-rw-r--r--
Sum.out
99
log
plain
-rw-r--r--
Sum.v
93
log
plain
-rw-r--r--
Tactics.out
256
log
plain
-rw-r--r--
Tactics.v
562
log
plain
-rw-r--r--
TranspModtype.out
89
log
plain
-rw-r--r--
TranspModtype.v
385
log
plain
-rw-r--r--
TypeclassDebug.out
864
log
plain
-rw-r--r--
TypeclassDebug.v
227
log
plain
-rw-r--r--
UnclosedBlocks.out
76
log
plain
-rw-r--r--
UnclosedBlocks.v
250
log
plain
-rw-r--r--
UnivBinders.out
4840
log
plain
-rw-r--r--
UnivBinders.v
4167
log
plain
-rw-r--r--
UsePluginWarning.out
14
log
plain
-rw-r--r--
UsePluginWarning.v
141
log
plain
-rw-r--r--
Warnings.out
187
log
plain
-rw-r--r--
Warnings.v
177
log
plain
-rw-r--r--
ZSyntax.out
578
log
plain
-rw-r--r--
ZSyntax.v
558
log
plain
-rw-r--r--
auto.out
544
log
plain
-rw-r--r--
auto.v
169
log
plain
-rw-r--r--
goal_output.out
98
log
plain
-rw-r--r--
goal_output.v
205
log
plain
-rw-r--r--
idtac.out
85
log
plain
-rw-r--r--
idtac.v
997
log
plain
-rw-r--r--
inference.out
559
log
plain
-rw-r--r--
inference.v
923
log
plain
-rw-r--r--
ltac.out
1472
log
plain
-rw-r--r--
ltac.v
1469
log
plain
-rw-r--r--
ltac_extra_args.out
378
log
plain
-rw-r--r--
ltac_extra_args.v
135
log
plain
-rw-r--r--
ltac_missing_args.out
1813
log
plain
-rw-r--r--
ltac_missing_args.v
384
log
plain
-rw-r--r--
names.out
275
log
plain
-rw-r--r--
names.v
228
log
plain
-rw-r--r--
onlyprinting.out
18
log
plain
-rw-r--r--
onlyprinting.v
107
log
plain
-rw-r--r--
qualification.out
173
log
plain
-rw-r--r--
qualification.v
324
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
276
log
plain
-rw-r--r--
set.v
154
log
plain
-rw-r--r--
simpl.out
198
log
plain
-rw-r--r--
simpl.v
148
log
plain
-rw-r--r--
subst.out
1242
log
plain
-rw-r--r--
subst.v
1588
log
plain
-rw-r--r--
unifconstraints.out
1487
log
plain
-rw-r--r--
unifconstraints.v
655
log
plain