参见Ltac中的Hintbase

编辑:

您正在尝试的操作目前在Ltac中不起作用。

https://github.com/coq/coq/issues/2417

你可以通过

• 将您的问题重新表述为一个单独的问题,您可以解释为什么需要这种自动化,有人可能会以不同的方式帮助您解决初始问题(不使用自动和数据库参数)

或

• 尝试一种新的Coq策略库,如 Ltac2

旧(坏)答案:

在Coq 8.7.2中,您需要的是 ident 参数类型。 根据定义,提示数据库由 识别号 :

Create HintDb ident [discriminated] 

(参见 https://coq.inria.fr/distrib/current/refman/tactics.html#Hints-databases 用于定义)

放置

Tactic Notation "test" ident(db) :=
  auto with db.

对我来说很好。

https://coq.inria.fr/distrib/current/refman/syntax-extensions.html#hevea_command236 包含允许的修饰符列表。