Use symbol ∗ for separating conjunction.

The old choice for ★ was a arbitrary: the precedence of the ASCII asterisk * was fixed at a wrong level in Coq, so we had to pick another symbol. The ★ was a random choice from a unicode chart.

The new symbol ∗ (as proposed by David Swasey) corresponds better to conventional practise and matches the symbol we use on paper.

Given that there is no real downside using the old notation, we should probably keep the old one, but "parsing only". I know that in practice we barely care about compatibility, but this change is quite large.

We can do that.

Note that contrary to other large changes (such as the renaming lately), it is very easy to port one's development to this change using a one line sed script.

Right, porting is easy, which is why I'd rather add that ´sed´ line to the README instead of leaving the old notation around forever.

Agreed with Ralf.

My sole concern with this merge request is that ∗ may look horrible in someone's font.

As Ralf pointed out by email, we have had way more invasive changes that we accepted while breaking compatibility drastically.

How does it look in gitlab by the way: ∗ versus *, and ∗ versus *

Edit: looks fine.

* and * do not show up at all on Thunderbird. So I put my veto on it. But ∗ is fine.

They did show up in this mail, but not in Robbert's. I believe that's related to the normal asterisk being a markdown special character.

That's correct, I edited my comment to escape the *.

Since nobody complained I propose to accept. @jung, @jjourdan is it OK to do that now?

Ok

Added 5 commits:

• 601ee3ee...6cb76aaa - 4 commits from branch master
• cc31476d - Use symbol ∗ for separating conjunction.

Compare with previous version

Ack.

Mentioned in commit 7d74f654

Status changed to merged