I have several proofs that follow identical structure. First of them can be finished with trivial, all the other ones with auto with foo_db, where foo_db is a hint database populated with hints after the first proof is complete. I'd like to write an Ltac procedure that uses auto with foo_db to solve all these proofs. However, when running that Ltac to solve the first of my proofs foo_db does not yet exist and so Coq complains: Error: No such Hint database: foo_db.. Is there a way to initialize an empty hint database?