diff options
| author | Pierre-Marie Pédrot | 2018-11-26 17:49:18 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-02 10:41:19 +0200 |
| commit | d4f43a59d5e1361e11943a35754e0feb27d37b15 (patch) | |
| tree | a5047b34d5117d23a20ad30bef8136428e61d8b8 | |
| parent | 99362197a42fdbf8d39f1cde0723389b5114dd98 (diff) | |
Document the Fast Name Printing option.
| -rw-r--r-- | CHANGES.md | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 14 |
2 files changed, 18 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md index 7f4f9a232b..5eb0c84c92 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -175,6 +175,10 @@ Vernacular commands - `Coercion` does not warn ambiguous paths which are obviously convertible with existing ones. +- A new flag `Fast Name Printing` has been introduced. It changes the + algorithm used for allocating bound variable names for a faster but less + clever one. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 3e8dd25ee0..e207a072cc 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -510,6 +510,20 @@ Requests to the environment .. seealso:: Section :ref:`locating-notations` +.. _printing-flags: + +Printing flags +------------------------------- + +.. flag:: Fast Name Printing + + When turned on, |Coq| uses an asymptotically faster algorithm for the + generation of unambiguous names of bound variables while printing terms. + While faster, it is also less clever and results in a typically less elegant + display, e.g. it will generate more names rather than reusing certain names + across subterms. This flag is not enabled by default, because as Ltac + observes bound names, turning it on can break existing proof scripts. + .. _loading-files: |