diff options
| author | Jason Gross | 2018-07-31 22:34:02 -0400 |
|---|---|---|
| committer | GitHub | 2018-07-31 22:34:02 -0400 |
| commit | acc7acfa0e8015b5785cb0f2d01acca2448e8197 (patch) | |
| tree | 481e7fdf9756f595c7ef10a5702199ca3fc13761 | |
| parent | 5e301f1a87c856eb22f2d219f940a99508bf23be (diff) | |
Camlp{4 => 5}
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 39f845d81c..37394386e6 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1457,7 +1457,7 @@ tactic language. Tactic notations obey the following syntax: .. [#no_associativity] Coq accepts notations declared as ``no associativity`` but the parser on which Coq is built, namely - Camlp4, currently does not implement ``no associativity`` and + Camlp5, currently does not implement ``no associativity`` and replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` is in fact ``left associativity``, for the purposes of parsing |