Revert "Notations: Trying using a notation with or w/o removal of coe…

[gares]

Fix #11033

Or course any other fix is fine to me

[gares]

This bug affects 8.10 too, if a new point release is to be made @vbgl can consider backporting this

[vbgl]

Can you please add a test-case corresponding to the bug report? Thanks.

[gares]

There you are, this is the test I've used for bisecting (plus grep COERCION, that should not succeed, since coercions should not be printed)

[gares]

Also 8.11 is affected, CC @ppedrot @mattam82 .

I don't know if a better fix can be provided in time for the release, I see this PR for the worst case scenario.

[herbelin]

@gares, thanks for the quick finding of the issue! If it is clear that #8890 is a change of semantics, I would not say that it is bug though, especially regarding this other expectation.

Since this is already released in 8.10, I'd be tempted to test the following cheap-to-implement improvement of the criterion used in #8890: look for notations which span the full application of the coercion to a term, rather than looking for a notation which applies to any partial prefix of the term as it is with #8890. By doing so, in the #11033 example, Notation COERCION x := (c x). would use the notation but Notation COERCION := c. would not. This looks like a reasonable compromise on guessing what the intent of the user is in defining a notation involving a coercion.

[JasonGross]

Since this is already released in 8.10, I'd be tempted to test the following cheap-to-implement improvement of the criterion used in #8890: look for notations which span the full application of the coercion to a term, rather than looking for a notation which applies to any partial prefix of the term as it is with #8890. By doing so, in the #11033 example, Notation COERCION x := (c x). would use the notation but Notation COERCION := c. would not. This looks like a reasonable compromise on guessing what the intent of the user is in defining a notation involving a coercion.

I would prefer this solution over simply reverting #8890

[herbelin]

See #11090 for the variant of #8890 which looks only for notations matching the fully applied coercion.

[ejgallego]

Superseeded by #11090