Pierre Courtieu
Pierre Courtieu
Hi. `proof-three-window-mode-policy ` is a customizable variable, so you will probably have abetter effect using `(customize-set-variable 'proof-three-window-mode-policy 'hybrid)`. . To know if a variable is a customizable one look at...
Tell me if this solves your problem.
FTR proofgeneral never used this information until now (the ascii underlining being much more robust). This is probably why this bug went unnoticed for so long. Side note: since ascii...
Thanks for this. Will this fix make it to 8.20 release or 8.21? No real big deal, just for documenting PG workaround.
I am not familiar with the printing commands but it looks correct to me. I don't see why this makes the `%scope` go beyond the margin. There should be a...
I see, so the inner box does not need a newline and then glue don't break either. I think the common practice is to consider "`)%scope`" as one unique printing...
Or maybe just put the`%scope` inside the same box as the parenthesis instead of after it? ```ocaml ... Ppcmd_box (Pp_hovbox 1, Ppcmd_glue [Ppcmd_string "("; ... Ppcmd_print_break (1, 0); Ppcmd_tag ("constr.variable",...
Thanks @SkySkimmer . We will try to get something working quickly.
What is the status of this issue pls?
Does it disappear if company-coq is unstalled.