issues
search
uwplse
/
fix-to-elim
Fixpoint to eliminator translation in Coq
MIT License
3
stars
5
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Coq 8.14
#17
agrarpan
closed
4 months ago
0
Ported plugin to Coq 8.13
#16
agrarpan
opened
4 months ago
0
Port fix-to-elim to Coq 8.11
#15
InnovativeInventor
opened
2 years ago
0
8.9.1
#14
tlringer
closed
3 years ago
0
first pass anonymization
#13
chandrakananandi
closed
4 years ago
0
first pass anonymization
#12
chandrakananandi
closed
4 years ago
0
Failure to preprocess Coq.ZArith.BinInt
#11
Ptival
closed
4 years ago
12
Illegal application (Non-functional construction)
#10
Ptival
opened
4 years ago
3
Problem with ssreflect tuple
#9
Ptival
closed
4 years ago
2
Aliasing `Vector` trips the pre-processing
#8
Ptival
closed
4 years ago
1
Recursively preprocess constants by default, with an "opaque" option to ignore constants
#7
tlringer
closed
4 years ago
0
Better evar_map hygiene
#6
tlringer
closed
5 years ago
0
Coq CI
#5
tlringer
opened
5 years ago
0
Clean code
#4
tlringer
opened
5 years ago
0
Update Coq version
#3
tlringer
opened
5 years ago
0
Update docs and tests to include Preprocess docs and tests from DEVOID
#2
tlringer
closed
5 years ago
0
License
#1
tlringer
closed
5 years ago
0