X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=114f2d9bbd0527432cdf37a8837df3eae2f85db3;hp=1f1229d66651b2a6d24a74fac77524b85242fdd0;hb=3282a2b78028238987a5a49e59d8e8d495aea0e1;hpb=af41ffb1692ae207554342ccdc3bf73abaa75a01

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 1f1229d..114f2d9 100644
--- 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''.