coq - Ltac : forall 仮説をインスタンス化する

Question

私は2つの新しい仮説を作成する戦術に取り組んでいます

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
.

was はh、分解する仮説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では完全に機能します。