Program functions can be declared as partial with "let/val partial".
Similarly to "diverges", partial code cannot be ghost, however it does not need to be
explicitly specified as partial.
Fixes#184.
Without an argument, break and continue refer to the innermost loop.
A label put over an expression sequence starting with a loop, can be
used as an optional argument for break and continue:
label L in
[ghost] ["tag"] [M.begin]
while true do
...
break L
...
done;
[...]
[end] [: unit]
In the square brackets are listed the constructions allowed between
the label declaration and the loop expression.
To install the Why3-related Vim files, just create a symbolic link:
ln -s "$(why3 --print-datadir)/vim" ~/.vim/bundle/why3
Thanks to Johanness Kanig for the suggestion.
