github jscoq/jscoq v0.11.0
JsCoq 0.11 "<-lib->"

latest releases: v0.17.1, v0.16.0, v0.15.1...
4 years ago
  • Project moved to
  • Port to Coq 8.11 (@ejgallego)
  • Ltac2 is now built from the included Coq source and loaded by
    default by the init package (@ejgallego)
  • Primitive floats are available. Note that writing .vo files that
    use primitive floats is not possible from jsCoq; this is due to the
    js runtime representation for integers being already a float, so
    Marshall will be confused. Only writing .vo files is
    problematic tho, you can however use primitive floats normally, and
    load .vo files that where compiled with coqc using primitive
    floats normally (@ejgallego)
  • Enforce explicit module prefix in Require statements for non-Coq
    packages, to avoid ambiguity (@corwin-of-amber)
  • Init options for finer control of jsCoq's behavior: show, focus,
    replace, and init_import (@corwin-of-amber)
  • Line numbers continue across code snippets on the same page. Useful
    for coqdoc-generated pages (@corwin-of-amber)
  • Accept dropped .coq-pkg files as packages to add to the current
    session (@corwin-of-amber)
  • Allow multiple directories for package files (@corwin-of-amber)

Don't miss a new jscoq release

NewReleases is sending notifications on new releases.