proofmode/notation.v · e3c56f9e10ea47cbf767516b1967af9dc8be7eaa · William Mansky / Iris

Forked from Iris / Iris

Source project has a limited visibility.

9 years ago

Add the zero-width spaces at the *end* of the lines, and a newline before the first context · e3c56f9e

Ralf Jung authored 9 years ago

Pros:
* It does not matter how editors render the 0-width space, everything is always aligned
* In ProofGeneral, there is no more incorrectn indentation of the first line

Cons:
* There is an empty line between the bar ending the Coq context, and the first Iris hypothesis

e3c56f9e

History

Add the zero-width spaces at the *end* of the lines, and a newline before the first context

Ralf Jung authored 9 years ago

Pros:
* It does not matter how editors render the 0-width space, everything is always aligned
* In ProofGeneral, there is no more incorrectn indentation of the first line

Cons:
* There is an empty line between the bar ending the Coq context, and the first Iris hypothesis