Create HintDb does not erase pre-existing hint db

doc/changelog/08-vernac-commands-and-options/19808-create-hintdb.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  :cmd:`Create HintDb` does not erase pre-existing hint databases
+  (`#19808 <https://github.com/coq/coq/pull/19808>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -329,7 +329,9 @@ and `Constants`, while implicitly created databases have the `Opaque` setting.
 
 .. cmd:: Create HintDb @ident {? discriminated }
 
-   Creates a new hint database named :n:`@ident`. The database is
+   If a hint database named :n:`@name` already exists, do nothing.
+
+   Otherwise creates a new hint database named :n:`@ident`. 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
@@ -340,6 +342,13 @@ and `Constants`, while implicitly created databases have the `Opaque` setting.
 
    By default, hint databases are undiscriminated.
 
+   .. warn:: @ident already exists and is {? not } discriminated
+      :name: mismatched-hint-db
+
+      `Create HintDb` will not change whether a pre-existing database
+      is discriminated.
+
+
 Hint databases defined in the Rocq standard library
 ```````````````````````````````````````````````````
 

tactics/hints.ml

@@ -1101,8 +1101,17 @@ type db_obj = {
   db_ts : TransparentState.t;
 }
 
-let cache_db {db_name=name; db_use_dn=b; db_ts=ts} =
-  searchtable_add (name, Hint_db.empty ~name ts b)
+let warn_mismatch_create_hintdb = CWarnings.create ~name:"mismatched-hint-db" ~category:CWarnings.CoreCategories.automation
+    Pp.(fun {db_name;db_use_dn} ->
+        str "Hint Db " ++ str db_name ++ str " already exists and " ++
+        (if db_use_dn then str "is not" else str "is") ++ str " discriminated.")
+
+let cache_db ({db_name=name; db_use_dn=b; db_ts=ts} as o) =
+  match searchtable_map name with
+  | exception Not_found -> searchtable_add (name, Hint_db.empty ~name ts b)
+  | db ->
+    (* AFAICT all DBs start with full transparent state so nothing to do with it *)
+    if Hint_db.use_dn db <> b then warn_mismatch_create_hintdb o
 
 let load_db _ x = cache_db x