coq - Ltac：实例化所有假设

Question

我正在研究一种可以创造两个新假设的策略

x0 : D
x0_Linked : P x0

从那种形式的假设

H : forall x : D, P x

这是我的 Ltac 代码：

Ltac mytactic h t x :=
    match type of h with
    | (forall (_: ?X1), _) =>  evar (x : X1) ; pose ( t := h x )
    | _ => idtac "Erreur: Aucun pour tout decomposable dans l'hypothese."
    end
.

wereh是要分解的假设，x新变量t的名称和新假设的名称。该策略按预期工作，但在证明结束时我得到了这个：

testproof< exact H0. 
All the remaining goals are on the shelf.

1 subgoal

subgoal 1 is:
 D

该evar策略似乎创建了一种名为 D 的新类型，而不是使用现有的类型。请注意，如果我使用

Coq< Variable x0 : D.

在 coqtop 中，它可以完美运行。