Skip to content

make binary wand/view shift connectives 'block' formated

Ralf Jung requested to merge ralf/wand-format into master

I noticed this formatting:

  PPPPPPPPPPPPPPPPP -∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗
  QQQQQQQQQQQQQQQQQQ

I don't think I like this -- when writing such terms myself, I apply the rule that if the RHS does not fit on a line, there is a linebreak just after the wand.

This adjusts the formatting so that Coq also prints things following that rule.

Merge request reports