Cannot create empty rewrite hint databases

[Tuplanolla]

Version

Coq 8.12.2

Operating system

Red Hat Enterprise Linux Workstation 7.4

Description of the problem

It is not possible to create an empty rewrite hint database.
There is no command to create one explicitly.
There is a way to create one implicitly,
but the result will contain at least one hint and
there is no command to remove it.
Besides, creating hint databases and scopes implicitly is deprecated or
at least considered to be bad form.

We can explicitly create and print hint databases and remove hints from them.

Create HintDb h.
Print HintDb h.

Hint Resolve eq_refl : h.
Print HintDb h.

Remove Hints eq_refl : h.
Print HintDb h.

Discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Cut: emp
For any goal ->

Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Cut: emp
For any goal ->
For eq ->   simple apply @eq_refl(level 0, pattern
            ?META161 = ?META161 :> ?META160, id 0)

Discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
Cut: emp
For any goal ->

We cannot explicitly create rewrite hint databases or
remove hints from implicitly created ones.

Fail Create Rewrite HintDb r.
Fail Print Rewrite HintDb r.

Hint Rewrite @eq_refl : r.
Print Rewrite HintDb r.

Remove Hints eq_refl : r.
Print Rewrite HintDb r.

The command has indeed failed with message:
Syntax error: illegal begin of vernac.
The command has indeed failed with message:
Rewriting base r does not exist.

Database r
rewrite -> @eq_refl of type forall (A : Type) (x : A), x = x

Database r
rewrite -> @eq_refl of type forall (A : Type) (x : A), x = x

Notes

There is also an inconsistency in how

• Hint Resolve eq_refl : h. works as expected,
• Hint Resolve @eq_refl : h. produces a warning about arbitrary terms as hints,
• Hint Rewrite @eq_refl : r. works as expected and
• Hint Rewrite eq_refl : r. causes an error during type inference.

Not being able to remove hints was already brought up in #13887.