fixes #1051 (rename lim_sup -> limn_sup)

[affeldt-aist]

Motivation for this change

fixes #1051

as (briefly) discussed during the last meeting https://github.com/math-comp/analysis/wiki/2023-10-16-Meeting

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.

[affeldt-aist]

TODO: add only parsing to deprecated notations! fixed (at least in the files concerned by this PR)

[affeldt-aist]

@CohenCyril the renaming is as we discussed during the last meeting, plus one name change that I made to be more uniform between the real and the ereal versions
I put "only parsing" format info for all deprecated (they shoud have been here from the start)

[CohenCyril]

I didn't know Coq accepted this... (only parsing syndefs...)

[CohenCyril]

Sure! I agree with the renaming. Can you tell me why the "only parsing" for lemmas (where are they printed anyway?)

[affeldt-aist]

I think that I only added them ("only parsing" format info) to Notation's. Indeed, I don't expect deprecation to work for lemma (I saw a few such faulty use of the deprecated pragmas in Rstruct.v
that I didn't try to fix).

[CohenCyril]

I meant: why bother putting only parsing on notations for lemma. What else than Print is going to display them anyway

[affeldt-aist]

I'll remove them asap.

[affeldt-aist]

I'll remove them asap.

Well, in fact, besides Print, they are useful to have correct error display.
If you apply the lemma for which a deprecated notation is not only parsing,
the error will report about the deprecated notation instead of the right lemma,
which is a bit disturbing (it happens a lot with measurable_* lemmas).

[CohenCyril]

I'll remove them asap.

Well, in fact, besides Print, they are useful to have correct error display. If you apply the lemma for which a deprecated notation is not only parsing, the error will report about the deprecated notation instead of the right lemma, which is a bit disturbing (it happens a lot with measurable_* lemmas).

I do not understand. It's good that the error is about the deprecated lemma, and that the warning notice gives the new lemma. Can you give me a concrete usecase, with a concrete error message and what's wrong with it. I tried to reproduce what you said but for me the result is unchanged whether I put only parsing or not...

e.g. whether I put measurable_fun_sqr as only parsing or not I get the following message, when I replace lebeqgue_measure.v line 1507, with:

   by apply: measurableT_comp (measurable_fun_sqr _) _; exact: measurable_funD.

it emits:

Warning: Notation measurable_fun_sqr is deprecated since mathcomp-analysis 0.6.3.
use `measurable_exprn` instead [deprecated-syntactic-definition,deprecated]

anyway...

[affeldt-aist]

For example, in the current state, if you apply, say, measurableT_comp in the second half of lebesgue_measure.v, if it fails, it fails with the error

Error: Cannot apply lemma emeasurable_funN

which is a bit puzzling at first sight.
With only parsing, at least the error message is

Error: Cannot apply lemma measurableT_comp

[CohenCyril]

Oh I undestand now!! Thanks for the clarification!

[CohenCyril]

This is really nontrivial, could you document it somewhere?

[affeldt-aist]

This is really nontrivial, could you document it somewhere?

What about an entry in CONTRIBUTING.md about how to write deprecated pragmas?

[affeldt-aist]

I added a few sentence in CONTRIBUTING.md