- 19 Apr, 2016 2 commits
-
-
Ralf Jung authored
FDor editors that display 0-width space with more than 0 width, this makes the indentation of assertions more consistent
-
Robbert Krebbers authored
newline before the first context" and "shuffle 0-width spaces around so they are distributed more evenly" This reverts commits e3c56f9e and 7fc1124c, which are workarounds for Coq bug https://coq.inria.fr/bugs/show_bug.cgi?id=4675 Also, this commit fixes the levels to avoid parantheses.
-
- 15 Apr, 2016 2 commits
-
-
Ralf Jung authored
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
-
Ralf Jung authored
-
- 11 Apr, 2016 1 commit
-
-
Robbert Krebbers authored
-