You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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)