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

coq.hb                                            December 2021                                        COQ.HB(1)