X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=e8aceb11a4586e03decbb2e9484b83f78f6338ed;hp=5e16f56ad6baa0209eed92e34c9159fd06d1da87;hb=35d3a59796735e5341389fa6a145f62dcea9c3fc;hpb=15df3430938d7175361b848de6578aea195e612f

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 5e16f56..e8aceb1 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -199,6 +199,7 @@ Section HaskFlattener.
   Set Printing Width 130.
 
   Context (hetmet_flatten : WeakExprVar).
+  Context (hetmet_unflatten : WeakExprVar).
   Context (hetmet_id      : WeakExprVar).
   Context {unitTy : forall TV, RawHaskType TV ★                                          }.
   Context {prodTy : forall TV, RawHaskType TV ★  -> RawHaskType TV ★ -> RawHaskType TV ★ }.
@@ -914,6 +915,13 @@ Section HaskFlattener.
           apply nd_rule.
           apply q.
           apply INil.
+        destruct (eqd_dec (g:CoreVar) (hetmet_unflatten:CoreVar)).
+          set (garrowfy_code_types (g wev)) as t.
+          set (RGlobal _ Δ nil (mkGlobal Γ t hetmet_id)) as q.
+          simpl in q.
+          apply nd_rule.
+          apply q.
+          apply INil.
         apply nd_rule; rewrite globals_do_not_have_code_types.
           apply RGlobal.
       apply (Prelude_error "found RGlobal at depth >0").