fix missing type-level equivalence in contra

[Tragicus]

Motivation for this change

The type-level equivalence was missing from the inference algorithm for contra.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[proux01]

Could the commit / PR titles and descriptions be more precise? It reads "fix contra" but then it seems to be mostly adding a type level equivalence, so I'm a bit lost.

[proux01]

The usual style in mathcomp rather seems to be something like

Suggested change

	Definition equivT_LR {S T} '(EquivT S_T _) : S -> T := S_T.
	Definition equivT_RL {S T} '(EquivT _ T_S) : T -> S := T_S.
	Definition equivT_LR {S T} (eq : equivT S T) : S -> T := let: EquivT S_T _ := eq in S_T.
	Definition equivT_RL {S T} (eq : equivT S T) : T -> S := let: EquivT _ T_S := eq in T_S.

[Tragicus]

Should I also change l.75?

[proux01]

Since this notation is used only on the three lines below (it is not exported), I'd rather remove it to avoid modifying the parser just for that.

[affeldt-aist]

the following line
"The ForallI implementation has to work around several Coq 8.12 issues"
suggest that some workarounds could be removed from the code

[Tragicus]

I think I remember asking [at]ggonthier, who said that the issues have not been fixed yet.

[Tragicus]

Could the commit / PR titles and descriptions be more precise? It reads "fix contra" but then it seems to be mostly adding a type level equivalence, so I'm a bit lost.

I changed the PR title and description, I will do the commit messages when I squash. IS that better?

[proux01]

Not really, this still doesn't tell what this type level equivalence is useful for, what problem it fixes (why it was "missing in the inference algorithm", could you give an example) and why it is defined here.

[Tragicus]

It was part of the code from [at]ggonthier I ported to define the contra tactic and I pruned a little too much. I am afraid I can not tell you why it is needed since I do not know. As for an example, #1173 does not compile without it (if you put its commit on top of master, wochoice.v fails at l.167).

[proux01]

Ok, thanks for the explanation! It would probably have made more sense to put it in #1173 then, but let's merge.

[affeldt-aist]

We merge it because otherwise contra will not work as expected but we'll issue about the lack of examples in the doc.