.\" DO NOT MODIFY THIS FILE!  It was generated by help2man 1.48.5.
.TH COQ.HB "1" "December 2021" "coq.hb " "User Commands"
.SH NAME
coq.hb \- Command line utility to apply patches generated by HB.
.SH DESCRIPTION
.PP
After building your project with logging enabled, eg
.IP
COQ_ELPI_ATTRIBUTES='hb(log(raw))' make
.PP
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.
.SS "usage:"
.TP
hb patch [\-f] <file.v>..
Applies the patches in <file.v.hb> to <file.v>.
\fB\-f\fR forces patch application even if the source file
is newer than the patch.
.TP
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>.
.TP
hb show <file.v.hb>..
Lists all the patches contained in <file.v.hb> (debugging).
.PP
Command line utility to apply patches generated by HB.
.PP
After building your project with logging enabled, eg
.IP
COQ_ELPI_ATTRIBUTES='hb(log(raw))' make
.PP
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.
.SS "usage:"
.TP
hb patch [\-f] <file.v>..
Applies the patches in <file.v.hb> to <file.v>.
\fB\-f\fR forces patch application even if the source file
is newer than the patch.
.TP
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>.
.TP
hb show <file.v.hb>..
Lists all the patches contained in <file.v.hb> (debugging).