There was an error while loading. Please reload this page.
Updated Home (markdown)
Renaming Coq -> Rocq
Updated The CertiRocq pipeline (markdown)
Updated The CertiCoq pipeline (markdown)
Updated The CertiRocq plugin (markdown)
Updated The CertiCoq plugin (markdown)
fix a bug in description of how to call certicoq_modify
Explain how to handle C global pointers into the Coq heap, with reference to certicoq-set-library
Updated Glue Code and FFI (markdown)
Created When C code allocates on the Coq heap (markdown)
Updated Memory Model and Garbage Collection (markdown)
Minor edits, and improve a bibliographic citation with URL