title: Problems adding new notation in Coq
body: <p>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 (<a href="https://coq.inria.fr/refman/user-extensions/syntax-extensions.html" rel="nofollow noreferrer">https://coq.inria.fr/refman/user-extensions/syntax-extensions.html</a>).</p>
  <p>I define my new scope with</p>
  <pre><code>Declare Scope myHoTT_scope.
  Delimit Scope myHoTT_scope with my.
  </code></pre>
  <p>Later I want to add &quot;*&quot; as an infix operator to the scope. I do this with</p>
  <pre><code>Infix &quot;*&quot; := concat (at level 40 , left associativity) : myHoTT_scope.
  </code></pre>
  <p>where concat is an already defined function. Coq accepts all of this. It raises no errors or warning. However, if I run</p>
  <pre><code>Locate &quot;*&quot;.
  </code></pre>
  <p>the only thing that is returned is the definition of &quot;*&quot; in type_scope and nat_scope. Additionally, if I try</p>
  <pre><code>Check (p * q)%my. 
  </code></pre>
  <p>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.</p>
  <p>** 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?</p>