issues
search
uwplse
/
coq-plugin-lib
Library of useful utility functions for Coq plugins
MIT License
12
stars
5
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Coq 8.14
#44
agrarpan
closed
3 months ago
0
Ported plugin to Coq 8.13
#43
agrarpan
opened
3 months ago
3
Port coq-plugin-lib to Coq 8.11
#42
InnovativeInventor
opened
2 years ago
0
Sound
#41
tlringer
opened
3 years ago
0
Merge 8.9.1 into master
#40
tlringer
closed
3 years ago
0
Abstracted getting hints.
#39
randair
closed
3 years ago
0
simpl back to greedy form
#38
randair
closed
3 years ago
0
Decompiler Sigma
#37
randair
opened
3 years ago
0
Intermediate custom tactics.
#36
randair
closed
3 years ago
0
Simplified rewrites.
#35
randair
closed
3 years ago
0
Fully working semicolons.
#34
randair
closed
3 years ago
0
Apply with implicit arguments.
#33
randair
closed
3 years ago
0
some anonymization
#32
ztatlock
closed
3 years ago
0
Decompiler
#31
randair
closed
4 years ago
0
Destruct applications of important functions into records.
#30
randair
closed
4 years ago
1
Logical operations on Props.
#29
randair
closed
4 years ago
1
Rewrite support in equtils
#28
randair
closed
4 years ago
2
Create utility procedures for module manipulation
#27
nateyazdani
closed
4 years ago
0
Fix PR from before
#26
tlringer
closed
5 years ago
0
Refactor coqterms (fixes #15)
#25
tlringer
closed
5 years ago
0
Credit Nate
#24
tlringer
closed
5 years ago
0
Refactor code that has to do with relating two terms
#23
tlringer
closed
5 years ago
0
File organization
#22
tlringer
closed
5 years ago
0
Comments
#21
tlringer
opened
5 years ago
0
Clean HOF type signatures
#20
tlringer
opened
5 years ago
0
Clean up / consolidate substitutions
#19
tlringer
opened
5 years ago
0
Move TODOs in code into issues
#18
tlringer
opened
5 years ago
0
Fix debruijn bugs, or use built-in Coq functions
#17
tlringer
opened
5 years ago
1
Favor econstr when possible instead of constantly converting
#16
tlringer
opened
5 years ago
0
Break coqterms into smaller files
#15
tlringer
closed
5 years ago
1
Name collision with reverse
#14
tlringer
closed
5 years ago
0
Address all warnings
#13
tlringer
opened
5 years ago
0
Remove unused functions
#12
tlringer
opened
5 years ago
0
Build process?
#11
tlringer
closed
5 years ago
0
Update to latest Coq version
#10
tlringer
opened
5 years ago
0
Clean code
#9
tlringer
opened
5 years ago
0
Better error messaging practices
#8
tlringer
opened
5 years ago
0
Use good evar_map hygiene
#7
tlringer
closed
5 years ago
0
Include in PUMPKIN PATCH build process
#6
tlringer
closed
5 years ago
0
Include in DEVOID build process
#5
tlringer
closed
5 years ago
0
Refactor code from DEVOID
#4
tlringer
closed
5 years ago
0
Refactor code from PUMPKIN PATCH
#3
tlringer
closed
5 years ago
0
Update docs
#2
tlringer
closed
5 years ago
0
License
#1
tlringer
closed
5 years ago
0