---

1

which are the levels effectively chosen in the current implementation of Coq

2

Coq accepts notations declared as no associative but the parser on which Coq is built, namely Camlp4, currently does not implement the no-associativity and replace it by a left associativity; hence it is the same for Coq: no-associativity is in fact left associativity

3

Tactic notations are just a simplification of the Grammar tactic simple_tactic command that existed in versions prior to version 8.0.