X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=c29963e3bfc6c9e1dbdf95259c7e2fe9068916e4;hp=b0c5b11180c4e2775354ec25704507d839f4bc01;hb=75a5863eb9fb6cdfa1f07e538f6f948ffec80331;hpb=148579e5c8f6b60209a442222b932cf59f163cca

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index b0c5b11..c29963e 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -826,10 +826,11 @@ Definition expr2proof  :
     destruct case_ELet; intros; simpl in *.
       eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
       eapply nd_comp; [ apply nd_llecnac | idtac ].
-      apply nd_prod; [ idtac | apply pf_let].
-      clear pf_let.
-      eapply nd_comp; [ apply pf_body | idtac ].
-      clear pf_body.
+      apply nd_prod.
+        apply pf_let.
+        clear pf_let.
+        eapply nd_comp; [ apply pf_body | idtac ].
+        clear pf_body.
       fold (@mapOptionTree VV).
       fold (mapOptionTree ξ).
       set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.