issues
search
lukaszcz
/
coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Other
210
stars
31
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
qauto breaks goal into multiple subgoals instead of solving or failing.
#183
sakekasi
opened
3 days ago
0
Adapt to coq/coq#19390 (goptions tables can discharge) + fix module substitution
#182
SkySkimmer
opened
1 week ago
1
Adapt to coq/coq#18973.
#181
rlepigre
closed
1 month ago
3
Proof General UI and kernel out of sync from aborting tactics?
#180
AndreasLoow
opened
3 months ago
2
Adapt w.r.t. coq/coq#18956.
#179
ppedrot
closed
3 months ago
2
Adapt to coq/coq#18938 (EConstr.ERelevance)
#178
SkySkimmer
closed
3 months ago
1
Please create a tag for Coq 8.19 in Coq Platform 2024.01
#177
rtetley
closed
3 months ago
1
Please create a tag for Coq 8.19 in Coq Platform 2024.01
#176
rtetley
closed
3 months ago
2
Support for Coq 8.19
#175
SnarkBoojum
closed
3 months ago
3
Adapt to coq/coq#18038 (rewrite rules)
#174
yannl35133
closed
5 months ago
1
hammer and coqserapi
#173
liuxingpeng520521
closed
6 months ago
1
simplify opam files in master
#172
palmskog
closed
8 months ago
0
Support for CVC5
#171
palmskog
opened
8 months ago
1
Adapt to coq/coq#17836 (case relevance outside case info)
#170
SkySkimmer
closed
8 months ago
1
Adapt w.r.t. coq/coq#18279.
#169
ppedrot
closed
8 months ago
1
switch to Docker Action CI for 8.18
#168
palmskog
closed
8 months ago
0
switch to Docker Action CI
#167
palmskog
closed
8 months ago
1
Please create a tag for Coq 8.18 in Coq Platform 2023.10
#166
rtetley
closed
8 months ago
2
Please create a tag for Coq 8.18 in Coq Platform 2023.10
#165
rtetley
closed
8 months ago
6
Support for Coq 8.18
#164
SnarkBoojum
closed
8 months ago
2
Adapt to coq/coq#17836 (sort poly)
#163
SkySkimmer
closed
8 months ago
1
Adapt to Coq PR #17987 which adds sigma to the API of search functions
#162
herbelin
closed
10 months ago
1
Adapt w.r.t. coq/coq#17768.
#161
ppedrot
closed
1 year ago
1
hammer and sauto output in response window don't give non-CoqHammer code meant to replace hammer and sauto statements.
#160
pr28416
closed
1 year ago
1
Adapt to coq/coq#17664 (goptions use Deprecation.t option instead of bool)
#159
SkySkimmer
closed
1 year ago
1
Adapt to coq/coq#17633 (decompose_app returns array not list)
#158
SkySkimmer
closed
1 year ago
1
fix dune build
#157
Alizter
closed
1 year ago
0
Bug with Strictprop?
#156
patrick-nicodemus
opened
1 year ago
2
Please create a tag for Coq 8.17 in Coq Platform 2023.03
#155
MSoegtropIMC
closed
1 year ago
1
Please create a tag for Coq 8.17 in Coq Platform 2023.03
#154
MSoegtropIMC
closed
1 year ago
4
Don't use Mltop.add_known_plugin
#153
SkySkimmer
closed
1 year ago
1
Feature Request: Environment to pre-populate lemmas into hammer.
#152
cbuschardt
closed
1 year ago
1
Don't force references at linking time
#151
SkySkimmer
closed
1 year ago
1
Adapt to coq/coq#16938 (staged options)
#150
SkySkimmer
closed
1 year ago
2
Adapt w.r.t. coq/coq#16903.
#149
ppedrot
closed
1 year ago
2
Adapt w.r.t. coq/coq#16442.
#148
ppedrot
closed
1 year ago
1
Trouble compiling 1.3.2+8.16
#147
SnarkBoojum
closed
1 year ago
3
Broken in coq CI
#146
SkySkimmer
closed
1 year ago
7
CoqHammer fails at easy mathcomp goals
#145
aleloi
opened
1 year ago
1
Syntax error for output of hammer
#144
skogsbaer
opened
1 year ago
1
Please create a tag for Coq 8.16 in Coq Platform 2022.09
#143
MSoegtropIMC
closed
1 year ago
7
Please create a tag for Coq 8.16 in Coq Platform 2022.09
#142
MSoegtropIMC
closed
1 year ago
1
Unfolding of notations
#141
skogsbaer
opened
1 year ago
0
No 2> /dev/null redirection
#140
skogsbaer
opened
1 year ago
0
Install non-user-facing programs in /usr/libexec
#139
SnarkBoojum
opened
2 years ago
1
Improve CoqHammer error message when 'predict' not found
#138
aleloi
opened
2 years ago
2
Build from source fails
#137
will-leeson
closed
2 years ago
1
Fix mistake in #136 causing fatal warning in Coq's CI
#136
ejgallego
closed
2 years ago
1
[coq] Use findlib name in add_known_plugin
#135
ejgallego
closed
2 years ago
1
`sauto` causes "Unable to handle arbitrary u+k <= v constraints."
#134
QinshiWang
opened
2 years ago
1
Next