walker (Aug 06 2022 at 21:52): walker (Aug 06 2022 at 21:52):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 ?
walker (Aug 06 2022 at 21:54):Also I see there are variants hv, v and 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
Emilio Jesús Gallego Arias (Aug 06 2022 at 23:47):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: Jun 04 2023 at 19:30 UTC