Avoid relying on subgoals order for refine

[maximedenes]

In one particular occurrence, it seems that the order of subgoals generated by refine was incorrect, and is fixed by coq/coq#7825

I'm afraid CompCert was relying on the strange order in which subgoals were generated. Here is a patch that makes it not depend on the order.

[bschommer]

The change looks good to me.

[jhjourdan]

Thanks for the patch.

This is a patch to MenhirLib, which should be first integrated into MenhirLib (here) and then backported to CompCert.

In this patch, you are using a new syntax for naming the goals introduced by refine. While I think this is a good feature for Coq to have, I would prefer not using it for MenhirLib, in order to stay compatible with older Coq version. Any suggestions?

[maximedenes]

I would prefer not using it for MenhirLib, in order to stay compatible with older Coq version. Any suggestions?

Unfortunately, I don't know how to not depend on the (wrong) order of subgoals otherwise.

[xavierleroy]

So, what should we do about this issue? In which version of Coq was the ?[X] notation introduced? Would Program Definition work better than refine here?

[xavierleroy]

Apologies if I'm becoming insistent, but we must do something about this PR.

@maximedenes do you know offhand in which version of Coq the ?[X] notation was introduced?

[maximedenes]

@xavierleroy sorry for the lack of reply. According to the reference manual, the naming of existential variables was introduced in Coq 8.5 ("Existential variables are referred to by identifiers rather than mere numbers"). I'm not 100% sure this changelog entry corresponds to the ?[X] syntax, though.

I'm also not sure if Program Definition works better in this context, as it is unclear to me which unification algorithm it uses.

Following @jhjourdan 's advice, I suggest we simply close this PR. I can test the syntax with an old Coq version and submit a Menhirlib PR. If something needs to be done for backporting to CompCert, I'll open an issue later.

[xavierleroy]

Thanks for the quick and kind reply.

Currently, CompCert supports Coq versions 8.8 to 8.11 (included). I would have no problems dropping 8.8, maybe even 8.9.

Let me close this issue as suggested. I'll backport any change made on MenhirLib upstream.