The CertiRocqC plugin

The CertiRocqC plugin (Require Import CertiRocqC.CertiRocqC) provides the exact same functionality as the CertiRocq Plugin, except that it runs a CertiRocq compiled version of the CertiRocq pipeline, i.e. CertiRocq but in C code rather than ML code.

Commands are simply prefixed with CertiRocqC rather than CertiRocq.

The CertiRocqCheck plugin

This plugin (Require Import CertiRocqCheck.Loader) provides a CertiRocq-compiled version of MetaRocq's safe checker, i.e., a verified type-checker for Rocq compiled with a verified compiler.

The plugin provides a single command CertiRocqCheck [global_reference] that typechecks a global reference and all its dependencies and prints its type or an error message.