在我的COQ开发中，我正在学习如何为我的问题领域量身定制的新策略Adam Chlipala教授。在该页面上，他描述了如何创建强大的自定义策略。将repeat与match结合。
现在，我已经有了一种强大的单发策略，auto。它将提示数据库中发现的步骤链条串在一起。我投入了一些努力来策划这些提示数据库，因此我也想继续使用它。
但是，这提出了一个问题。尚不清楚将auto的功能合并到定制策略中的"正确"方法。
例如，由于（根据其页面）auto总是解决目标，要么什么都不做，因此将其放入循环中并不比循环后一次调用一次。
要查看为什么这不是理想的选择，请考虑一种假设的方式来直接称为auto的单个"步骤"，如果它可以进行更改（而不是在解决目标时，则成功），否则会失败。这种单步可以与匹配重复循环中的自定义行为交织在一起，从而使我们能够例如try contradiction或try congruence在搜索树中的中间点处。
是否有将auto的功能合并到自定义策略中的良好设计模式？
可以将auto的行为分解为我们可以使用的"单步"策略？
我要做的是将其他策略纳入auto。您可以使用Hint Extern num pat => mytactic : mybase命令，其中num是优先级数字（0是最高优先级），pat应使用提示时要过滤的模式，并且mytactic和mybase当然是您要应用的策略，并且是基础您想将提示添加到（请勿使用默认的core；而不是使用auto with mybase来调用它；如果您不想在搜索中包含core基础的引理，请添加伪造的基础nocore：auto with mybase nocore）。
如果您开始非常依赖auto，我会切换到几乎等效但表现更好的typeclasses eauto with mybase。与其名称所暗示的相反，它是一种通用策略，与类型类别无关（只要您明确提供应在其应有的提示基础）。要知道的主要行为差异之一是默认情况下搜索深度无限。因此，请注意可能的无限循环或使用变体typeclasses eauto num with mybase。