diff options
| author | Vincent Laporte | 2019-04-03 08:45:09 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-03 08:45:09 +0000 |
| commit | b45d4425b760b4e6346df4ea19f24d5c1e84b911 (patch) | |
| tree | 0e8ed49374addec3e100d8e4c239b511cf7234bc /doc | |
| parent | ae3c0e70f1d3f8d8d7c338ffd18b179968e920aa (diff) | |
| parent | d4f43a59d5e1361e11943a35754e0feb27d37b15 (diff) | |
Merge PR #9078: Provide a faster bound name generation algorithm through a flag
Ack-by: jfehrle
Ack-by: ppedrot
Reviewed-by: vbgl
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 14 |
1 files changed, 14 insertions, 0 deletions
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: |