Reference Manual | The Coq Proof Assistant

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.