SkySkimmer coq-ltac2-compiler issues

SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1

5 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

Fix Array.empty precompilation

#25 SkySkimmer closed 7 months ago
0
Incorrect compilation of Array.empty

#24 SkySkimmer closed 7 months ago
0
Adapt to coq/coq#18624 (Tac2ffi / Tac2val split)

#23 SkySkimmer closed 9 months ago
1
Put safety thunking in auxiliary function

#22 SkySkimmer closed 10 months ago
0
More precise monad thunking

#21 SkySkimmer closed 12 months ago
1
Translate non recursive let to nontac expr when possible

#20 SkySkimmer closed 12 months ago
0
Monad-thunk every nontrivial nontac_expr

#19 SkySkimmer closed 12 months ago
3
Silence warning in test

#18 SkySkimmer closed 12 months ago
0
Compilation produces code in incorrect order

#17 Janno closed 12 months ago
6
Assertion failed in `force_nontac_expr`

#16 Janno closed 12 months ago
1
Fix mutable skipping in recursive mode

#15 SkySkimmer closed 1 year ago
0
Mutable definitions lead to dynlink errors

#14 Janno closed 1 year ago
3
Fix support for ocaml < 4.13 (avoid String.for_all)

#13 SkySkimmer closed 1 year ago
0
Basic support for Ltac2 Backtrace / Ltac Profiling

#12 SkySkimmer opened 1 year ago
0
Support unicode in identifiers

#11 SkySkimmer closed 1 year ago
0
Experiment with optimization flags

#10 SkySkimmer opened 1 year ago
0
Update README.md

#9 SkySkimmer closed 1 year ago
0
Handle backtraces and profiling

#8 SkySkimmer opened 1 year ago
0
Ahead of time compilation

#7 SkySkimmer opened 1 year ago
3
OCaml does not support unicode binders?

#6 Janno closed 1 year ago
1
Avoid OCaml keywords

#5 SkySkimmer closed 1 year ago
0
Syntax error in generated code (need to avoid ocaml keywords)

#4 Janno closed 1 year ago
0
Adapt to coq/coq#18139 (pr_tacref takes avoid set)

#3 SkySkimmer closed 1 year ago
1
fix bugs (literal negative int, literal string had issues)

#2 SkySkimmer closed 1 year ago
0
Put back hardcoded primitives

#1 SkySkimmer closed 1 year ago
0