issues
search
mit-plv
/
coqutil
Coq library for tactics, basic definitions, sets, maps
MIT License
42
stars
24
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Please pick the version you prefer for Coq 8.16 in Coq Platform 2022.09
#71
MSoegtropIMC
closed
1 year ago
6
Bump etc/coq-scripts from `d85c149` to `5116cc9`
#70
dependabot[bot]
closed
2 years ago
1
Bump etc/coq-scripts from `0ca86bb` to `d85c149`
#69
dependabot[bot]
closed
2 years ago
1
Bump etc/coq-scripts from `0ca86bb` to `3ad4791`
#68
dependabot[bot]
closed
2 years ago
1
Weird Makefile logic?
#67
ejgallego
closed
2 years ago
8
Adapt w.r.t. coq/coq#16004
#66
Alizter
closed
2 years ago
4
coqutil.Z.bitblast not found in 8.13
#65
JasonGross
closed
1 year ago
3
Add `list_diff_length` lemma to coqutil
#64
pratapsingh1729
closed
2 years ago
0
Bump etc/coq-scripts from `7e68a28` to `0ca86bb`
#63
dependabot[bot]
closed
2 years ago
1
Bump etc/coq-scripts from `3be05c7` to `7e68a28`
#62
dependabot[bot]
closed
2 years ago
1
Please stop emailing me when tested fails to update
#61
JasonGross
closed
1 year ago
1
Bump actions/checkout from 2 to 3
#60
dependabot[bot]
closed
2 years ago
2
Properly deprecate combine and split
#59
proux01
closed
2 years ago
8
Restore compatibility with fiat-crypto
#58
JasonGross
closed
2 years ago
1
please update `tested` branch
#57
SkySkimmer
closed
2 years ago
4
hooking `word` into `lia`
#56
JasonGross
opened
2 years ago
1
Merging fiat-crypto utilities into coqutil?
#55
JasonGross
opened
2 years ago
2
Update job names in named-jobs
#54
JasonGross
closed
2 years ago
0
Try naming the jobs in coq.yml
#53
JasonGross
closed
2 years ago
1
Build fails on 8.11
#52
JasonGross
closed
2 years ago
10
improve LittleEndianList, deprecate LittleEndian
#51
andres-erbsen
closed
2 years ago
0
Bump etc/coq-scripts from `c34a5e9` to `3be05c7`
#50
dependabot[bot]
closed
2 years ago
1
Bump etc/coq-scripts from `b66ed67` to `c34a5e9`
#49
dependabot[bot]
closed
2 years ago
1
add Tactics.ident_of_string
#48
andres-erbsen
closed
2 years ago
0
add Tactics.ident_of_string
#47
andres-erbsen
closed
2 years ago
0
import Macros.ident_to_string from bedrock2
#46
andres-erbsen
closed
2 years ago
0
8.11 compat
#45
JasonGross
closed
2 years ago
2
eradicating LittleEndian.combine
#44
andres-erbsen
opened
2 years ago
2
Support 8.11
#43
andres-erbsen
closed
3 years ago
0
set Default Proof Using "All" in every Section
#42
andres-erbsen
closed
3 years ago
2
Compatibility with older versions of Coq
#41
JasonGross
closed
3 years ago
3
Partial compatibility with Coq 8.11
#40
JasonGross
closed
3 years ago
2
Add `Proof using` directives
#39
JasonGross
closed
3 years ago
14
Partial compatibility with Coq 8.12
#38
JasonGross
closed
3 years ago
0
Add boolean list equality decider
#37
jadephilipoom
closed
3 years ago
1
Added list update(s) definition and lemmas
#36
bdiehs
closed
3 years ago
0
Future proof ZLib.v and div_mod_to_equations.v
#35
mrhaandi
closed
3 years ago
2
LittleEndian.combine should not inline tuple.to_list
#34
andres-erbsen
closed
2 years ago
3
Avoid admits in symmetry test code
#33
tchajed
closed
3 years ago
1
Get of list z at app
#32
andres-erbsen
closed
4 years ago
2
Encoding functions with finite support as maps
#31
andres-erbsen
closed
4 years ago
6
Avoid using admit even in tests
#30
tchajed
closed
3 years ago
1
add | 10 to new Reflexive, Symmetric, and Transitive instances
#29
jadephilipoom
closed
4 years ago
2
New set lemmas
#28
jadephilipoom
closed
4 years ago
2
New list lemmas
#27
jadephilipoom
closed
4 years ago
0
Finish proving SortedList.map_ok
#26
mdempsky
closed
4 years ago
1
It would be better if coqutil used no axioms
#25
JasonGross
opened
4 years ago
5
There is no validate target, and if there were one, it would fail
#24
JasonGross
opened
4 years ago
0
Remove a strict_order axiom
#23
JasonGross
closed
4 years ago
0
coqutil.Map.SortedListString.map cannot be extracted
#22
JasonGross
opened
4 years ago
5
Previous
Next