mi.ki

> While the title says this PR introduces new alias names, it seems that it changes the default keyword. I am not sure we all agree on doing that ......

Thanks for spotting that, I reverted my changes in the two respective error messages now and added explanatory comments. Yep, in the link that I had provided, Dafny also compares...

I had implemented such an alias some years ago, but apparently this did not survive the release cycles. Shouldn't be a problem to reintroduce it though, in my opinion.

@fab918 I just took a look, but found out I did not introduce an alias for `loop_modifies` or `loop_writes`, but for `loop_variant` and `assigns` (yet another standard from somewhere else,...

@fab918 I created a new branch which should hopefully fix the previously lost changes and also add the two keywords from OpenJML. Maybe, you can test whether it works for...

It's been a while and after various internal discussions, the PR #3365 made it onto the main branch. So, @fab918, if you are still around, feel free to use it!

@flo2702 I just wanted to take a look at the bug and the patch or fix you mentioned. However, I cannot find the proposed patch, so could you maybe give...