Make "Found no matching notation to enable or disable." a warning

[proux01]

instead of an error

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

[herbelin]

The PR is nice for an "interactive"/"primary" use of Disable, but for a Imported deactivation on a non Imported notation, I believe something has to be done in the open_notation_toggle function, I recommend just ignoring the failure.

[herbelin]

No, my comment is wrong. Let me think again.

[herbelin]

I updated my comment. I would simply ignore the absence of a notation when deactivation comes from an Import.

Here is another variant of the Zulip example, showing a desynchronisation of imports:

(* comp.v *)
Definition comp {A B C} (f : B -> C) (g: A -> B) : A -> C := 
    fun a => f (g a).

Notation " g '\o' f " := (comp g f) (at level 40, left associativity).
Check ((@id nat) \o (@id nat)).

(* comp_utf.v *)
Require Import NotationTest.comp.

Disable Notation "\o".

Notation " g '∘' f " := (comp g f) (at level 40, left associativity).

(* comp_utf2.v *)
Require Import NotationTest.comp_utf.

Enable Notation "\o".

and

(* user.v*)
Require Import comp.
Require comp_utf.
Locate "\o". (* Notation " g '\o' f " := (comp g f) (default interpretation) *)
Require Import comp_utf2. (* Error: Found no matching notation to enable or disable *)

[proux01]

@herbelin do you want to merge this or should I close it? (I unfortunately do'nt have time to do anything better in the foreseable future)

[herbelin]

It brings something so I'm leaning towards merging.

[herbelin]

More convenient than an error.

[herbelin]

@coqbot merge now

[coqbot-app]

@herbelin: You cannot merge this PR because:

• There is still a needs: full CI label.
• No milestone has been set.

[herbelin]

@coqbot run full ci

[proux01]

@herbelin unimath failure is unrelated (c.f. #18726 )

[herbelin]

OK

@coqbot merge now