usage:¶

hb patch [-f] <file.v>..

Applies the patches in <file.v.hb> to <file.v>. -f forces patch application even if the source file is newer than the patch.

hb reset <file.v>..

Erases all generated code from source file. It does nothing if the file is not patched. If a patch file <file.v.hb> exists it is renamed to <file.v.hb.old>.

hb show <file.v.hb>..

Lists all the patches contained in <file.v.hb> (debugging).

Command line utility to apply patches generated by HB.

After building your project with logging enabled, eg

COQ_ELPI_ATTRIBUTES='hb(log(raw))' make

each file.v file contanining calls to HB is paired with a file.v.hb patch file which can be applied by this utility. You can also use COQ_ELPI_ATTRIBUTES='hb(log)' to get terms printed in a nicer, more compact, way but without all details they may not be parsable without manual editing.

usage:¶

hb patch [-f] <file.v>..

Applies the patches in <file.v.hb> to <file.v>. -f forces patch application even if the source file is newer than the patch.

hb reset <file.v>..

Erases all generated code from source file. It does nothing if the file is not patched. If a patch file <file.v.hb> exists it is renamed to <file.v.hb.old>.

hb show <file.v.hb>..

Lists all the patches contained in <file.v.hb> (debugging).