Coq：Ltac内部的“依赖感应”

在Ltac中,依赖性归纳对我来说似乎有所不同,而不是.

以下工作正常：

Require Import Coq.Program.Equality.

Goal forall (x:unit) (y:unit),x = y.
intros.
dependent induction x.
dependent induction y.
trivial.
Qed.

依赖感应在这里是过度的,因为破坏工作得很好.此外,如果Ltac用于帮助,则无需在校对脚本中命名要销毁的东西：

Ltac ok :=
  match goal with
    | [H : unit |- _] => destruct H
  end.

Goal forall (x:unit) (y:unit),x = y.
intros.
ok.
ok.
trivial.
Qed.

但是,当依赖感应取代destruct时,相同的Ltac会失败：

Ltac wat :=
  match goal with
    | [H : unit |- _] => dependent induction H
  end.

Goal forall (x:unit) (y:unit),x = y.
intros.
wat.

(*
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).
*)

设置Ltac Debug没有提供额外的有用信息,除了依赖感应实际上是在x和y上尝试.

奇怪的是,如果我在没有匹配的情况下将依赖感应包装在另一个Ltac中,并将其应用于一个等于我实际想要执行感应的术语,那么一切都顺利进行：

Ltac go H := let z := fresh in remember H as z; dependent induction z; subst H.

Ltac why :=
  match goal with
    | [H : unit |- _] => go H
  end.

Goal forall (x:unit) (y:unit),x = y.
intros.
why.
why.
trivial.
Qed.

这里发生了什么,为什么依赖感应似乎依赖于上下文？

解决方法

这确实是一个错误,并于2015年3月修复.