---
name: "coq.hb"
section: "1"
platform: "linux"
package: "coq-hierarchy-builder"
version: "1.4.0-2+b6"
release: "Debian 12 (Bookworm)"
platforms: ["linux"]
url: "https://new.carta.tech/coq.hb"
---

# coq.hb(1)

Command line utility to apply patches generated by HB.

## NAME

coq.hb - Command line utility to apply patches generated by HB.

## DESCRIPTION

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).

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).