Coq 8.6

These are the changes necessary to make this compatible with Coq 8.6. Most of the changes are fine (and of the category "no idea why this worked in 8.5" or "the statement of a lemma changed in the 8.6 libs"), except for the horribleness in perm_incl.v. I played around a little but found no good way to restore the term into the state Coq 8.5 put it in -- and the goals I end up in otherwise (if I just remove the change) look fairly unsolvable.

Cc @jjourdan @robbertkrebbers

It seems like the behaviour of simpl has changed. Again. I'll have a look at this.

Added 1 commit:

• 718290e1 - Remove a warning about a [ty_of_st], better compatibility fix in [perm_incl.v].

Compare with previous version

I think I found something better now.

simpl wasn't really used previously; it was relying on apply to produce a top-level *

Ah, that indeed looks much better. But it's not 8.5-compatible any more, is it -- so we have to wait with merging?

simpl wasn't really used previously; it was relying on apply to produce a top-level *

Oh, you added the //=. Well, so what changed are the heuristics of the unification algorithm. Again.

But it's not 8.5-compatible any more, is it -- so we have to wait with merging?

I have not tried, but I guess it should be compatible. I don't see why it should not.

Unmarked this merge request as a Work In Progress

Indeed it works in Coq 8.5. I was expecting trouble because of the cbn.

Mentioned in commit ed37ada5

Status changed to merged