X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=1f1229d66651b2a6d24a74fac77524b85242fdd0;hp=35373a76657a4ff168a0f9f260dd2efbbdcf4cf2;hb=d97b00a6ff6e8e2244927d17bda4b9762fc3d716;hpb=6a7c6977507488245ba4b8cabcf323920c25baef

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 35373a7..1f1229d 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -1189,7 +1189,7 @@ Definition expr2proof  :
         inversion H.
 
     destruct case_ELet; intros; simpl in *.
-      eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
+      eapply nd_comp; [ idtac | eapply RLet ].
       eapply nd_comp; [ apply nd_rlecnac | idtac ].
       apply nd_prod.
       apply pf_let.