I was under the impresion that
hov addes n spaces before a block of code, but I was totally wrong, All I was able to understan is that it is used to create boxes, but what extactly are those boxes supposed to do? Also if they are not for creating spaces/tabs, is there an automatic way to auto indent code block when doing custom extraction plugin ?
Also I see there are variants
hov but I cannot guess what each is supposed to do ? I assume h is for horizontal something and v is for vertical but I cannot understand the semantics
The semantics are indeed tricky; Coq boxes are mapped directly to OCaml's Format boxes, see the docs https://v2.ocaml.org/api/Format.html
Last updated: Feb 05 2023 at 20:03 UTC