X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=b14a53e8f23ca3e84921e9a1d126b599c52b70eb;hp=3aee2197d4534b90b053b68160dbd3338141b16a;hb=e4fcbccb71fc54544e9acc62e95d1d15ec86294b;hpb=75a0b52b9937ab6b68ed98cc24281bc9153e96b9

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.