[MC2] Adapt to math-comp/math-comp#1131

[pi8027]

Motivation for this change

This PR makes the hierarchy-builder branch (#951) compatible with math-comp/math-comp#1131. The issue stems from the fact that the parsing of (_ \; _) _ uses the \; notation defined in the classical_set_scope.

We probably should close the classical_set_scope and localize its use, e.g.,

Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.

Things done/to do

• [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

• [ ] added corresponding documentation in the headers

Compatibility with MathComp 2.0

• [ ] I added the label TODO: HB port to make sure someone ports this PR to
  the hierarchy-builder branch or I already opened an issue or PR (please cross reference).

Automatic note to reviewers

Read this Checklist and put a milestone if possible.

[proux01]

Why not putting the _ \; _ notation in function_scope?

[pi8027]

@proux01 That's because that does not fix the issue. I thought function_scope should be locally opened for the left-hand side of a function application, but it is not?

[pi8027]

Reported: rocq-prover/rocq#18372

[proux01]

Apparently not indeed. In master / future 8.19, an explicit cast t : _ -> _ opens function_scope in t but t x does not. Maybe something that could be tried in Coq.

[pi8027]

CI green.

[affeldt-aist]

Sorry for the lag, I was super busy. So I guess there was a conflict of notation and you judged that since this notation was used seldom used in this file it was right to remove it, is that it?

[proux01]

Yes

[affeldt-aist]

@pi8027 can you explain the logic? it looks like you removed the notation at some places but not at others?

[pi8027]

@affeldt-aist It seems that _ \; _ declared in the classical_set_scope has precedence over the _ \; _ local notation which I removed. I have no explanation for how math-comp/math-comp#1131 triggered this change, but MathComp analysis does not seem to use notation scopes correctly anyway.

[affeldt-aist]

MathComp analysis does not seem to use notation scopes correctly anyway.

You mean for example that we should be more careful when setting that arguments of definitions such that:

Arguments measurable {d}%measure_display_scope {s} _%classical_set_scope.

?

[pi8027]

@affeldt-aist Yes, and we should first understand how Coq interprets notations: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#notation-scopes

[affeldt-aist]

Thanks for the tip!