add support for flattening recursive-let

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

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 0d90d4c..3dbc81f 100644 (file)
--- a/src/HaskProofToStrong.v
+++ b/src/HaskProofToStrong.v
@@ -964,7 +964,7 @@ Section HaskProofToStrong.
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
     refine (X_ ((update_xi ξ t (leaves varstypes)))
     refine (bind ξvars = fresh_lemma' _ y _ _ _ t H; _). apply FreshMon.
     destruct ξvars as [ varstypes [ pf1[ pf2 pfdist]]].
     refine (X_ ((update_xi ξ t (leaves varstypes)))

-      (vars,,(mapOptionTree (@fst _ _) varstypes)) _ >>>= fun X => return _); clear X_.  apply FreshMon.
+      ((mapOptionTree (@fst _ _) varstypes),,vars) _ >>>= fun X => return _); clear X_.  apply FreshMon.

     simpl.
     rewrite pf2.
     rewrite pf1.
     simpl.
     rewrite pf2.
     rewrite pf1.