SkySkimmer/coq-ltac2-compiler

Issues

• Incorrect compilation of Array.empty

  #24 opened 2 months ago
  0

• Compilation produces code in incorrect order

  #17 opened 7 months ago
  6

• Assertion failed in `force_nontac_expr`

  #16 opened 7 months ago
  1

• Mutable definitions lead to dynlink errors

  #14 opened 8 months ago
  3

• Experiment with optimization flags

  #10 opened 8 months ago
  0

• Handle backtraces and profiling

  #8 opened 8 months ago
  0

• Ahead of time compilation

  #7 opened 8 months ago
  2

• OCaml does not support unicode binders?

  #6 opened 8 months ago
  1

• Syntax error in generated code (need to avoid ocaml keywords)

  #4 opened 8 months ago
  0