Apply suggestions from code review

Co-authored-by: Jim Fehrle <[email protected]>

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 <https://github.com/coq/coq/pull/19808>`_,
   by Gaëtan Gilbert).

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