Problems adding new notation in Coq

Question

I'm trying to define a new notation scope and add notation to this scope in Coq. I'm following the guidance of this page in the Coq manual (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html).

I define my new scope with

Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.

Later I want to add "*" as an infix operator to the scope. I do this with

Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.

where concat is an already defined function. Coq accepts all of this. It raises no errors or warning. However, if I run

Locate "*".

the only thing that is returned is the definition of "*" in type_scope and nat_scope. Additionally, if I try

Check (p * q)%my. 

I just receive errors stating that p should be of type nat. I can't tell why Coq doesn't seem to pick up this new notation. I followed the instructions to the letter and Coq gives no errors.

** Edit **, I found the problem. I had the definition of the new notation tucked inside a Section so its definition was not accessible from outside the section. I guess it is not possible to define global notation from within a section?

Answer 1

As you discovered yourself, indeed new notations inside a section cannot be forced to be global. At least, that’s what I understand from the reference manual here. And trying the export and global attributes to a notation command indeed fails.