coq - Ltac：使用回溯重复策略 n 次

Question

假设我有一个像这样的策略（取自 HaysTac），它搜索一个参数来专门化一个特定的假设：

Ltac find_specialize_in H :=
  multimatch goal with
  | [ v : _ |- _ ] => specialize (H v)
end.

但是，我想写一个策略来搜索n参数来专门化一个策略。关键是它需要回溯。例如，如果我有以下假设：

y : T
H : forall (x : T), x = y -> P x
x1 : T
x2 : T
Heq : x1 = y

如果我写do 2 (find_specialize_in H)，它可能会选择x2实例化它，然后尝试找到第二个参数失败。所以我需要我的重复循环能够回溯它选择专门化早期参数的参数。

是否有可能做到这一点？我怎样才能创建一个回溯其先前迭代选择的策略循环？