let RCut take a left environment as well

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

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 113955f..35373a7 100644 (file)
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -961,7 +961,7 @@ Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
       destruct q.
       simpl in *.
       apply n.
       destruct q.
       simpl in *.
       apply n.

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+    eapply nd_comp; [ idtac | eapply RCut' ].

       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply IHX1.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply IHX1.

@@ -1019,7 +1019,7 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree  :
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 
 
   set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
 

-    eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+    eapply nd_comp; [ idtac | eapply RCut' ].

       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply q.
       eapply nd_comp; [ apply nd_llecnac | idtac ].
       apply nd_prod.
       apply q.