X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=3dbc81f7cd79c2eca5c94205873246b6cc9db51f;hp=0d90d4c6c128d6f58f3e74b46ae4c5c0457b1ec3;hb=3282a2b78028238987a5a49e59d8e8d495aea0e1;hpb=d5f12624745edf327b49e515a1ebb5aeb265b70c;ds=sidebyside

diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v
index 0d90d4c..3dbc81f 100644
--- 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)))
-      (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.