X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FHaskProofToStrong.v;h=b14a53e8f23ca3e84921e9a1d126b599c52b70eb;hb=1c1cdb9014f409248ca96b677503719916b2b477;hp=3aee2197d4534b90b053b68160dbd3338141b16a;hpb=1cfe65d4e2d3292cc038882d8518dd7a48e2c40a;p=coq-hetmet.git diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 3aee219..b14a53e 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -569,7 +569,6 @@ Section HaskProofToStrong. destruct case_RGlobal. apply ILeaf; simpl; intros; refine (return ILeaf _ _). apply EGlobal. - apply wev. destruct case_RLam. apply ILeaf.