[Iris-Club] ∗ for separating conjunction

[Robbert Krebbers]

Hi all,

Dave Swasey recommended to use the symbol ∗ for separating conjunction 
(instead of the current ★) because it looks nicer and better matches 
conventional practice. I have created a merge request, see:

   https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/21

Please let me know ASAP (∗) if you are opposed, for example, because you 
cannot distinguish ∗ and * in your favorite font.

Robbert

(∗) If we perform this change, I would like to use the new symbol in the 
proof mode paper,  whose camera ready version is due Monday.