add support for flattening recursive-let

[coq-hetmet.git] / src / HaskStrongToProof.v

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 35373a7..114f2d9 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -997,7 +997,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
   eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
   clear z.
 
-  set (@factorContextRightAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
+  set (@factorContextLeftAndWeaken''  Γ Δ  pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
   unfold passback in *; clear passback.
   unfold pctx in *; clear pctx.
   set (q' disti) as q''.
@@ -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.