From 278a2aa098e0734c7c86e7274809caff26b01e64 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Dec 2024 14:51:04 +0100 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Jim Fehrle --- .../08-vernac-commands-and-options/19808-create-hintdb.rst | 2 +- doc/sphinx/proofs/automatic-tactics/auto.rst | 5 ++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst b/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst index 042d9ac178f2..4608a48cb8f2 100644 --- a/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst +++ b/doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst @@ -1,4 +1,4 @@ - **Changed:** - :cmd:`Create HintDb` does not erase pre-existing hint databases + :cmd:`Create HintDb` no longer erases pre-existing hint databases (`#19808 `_, by Gaëtan Gilbert). diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index f1c96da78b99..d4d66ec86fe0 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -329,9 +329,8 @@ and `Constants`, while implicitly created databases have the `Opaque` setting. .. cmd:: Create HintDb @ident {? discriminated } - If a hint database named :n:`@name` already exists, do nothing. - - Otherwise creates a new hint database named :n:`@ident`. The database is + If there is no hint database named :n:`@name`, creates a new hint database + with that name. Otherwise, does nothing. The database is implemented by a Discrimination Tree (DT) that serves as a filter to select the lemmas that will be applied. When discriminated, the DT uses transparency information to decide if a constant should considered rigid for