Confusing notation

Hi,

PROSA defines the following:

./implementation/refinements/task.v:Notation "{| 'id:' c1 'cost:' c2 'deadline:' c3 'arrival:' c4 'priority:' c5 }" := {|

This creates much confusion IMHO. Tweaking the notation for records is unexpected, and without proper documentation, this can be easily overlooked when trying to use existing code snippets.

I understand why you want this, but I would recommend a different notation, e.g. {/ .. /}, to be more visible.