X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=ae9960559b5e305fe0006142cdc247b9c5d2a3f2;hp=5e16f56ad6baa0209eed92e34c9159fd06d1da87;hb=1c1cdb9014f409248ca96b677503719916b2b477;hpb=dac68fdf6d495ed60d3e4c5738c27ca7fffc1399

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 5e16f56..ae99605 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -17,7 +17,8 @@ Require Import HaskCoreTypes.
 Require Import HaskCoreVars.
 Require Import HaskWeakTypes.
 Require Import HaskWeakVars.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
 Require Import HaskStrongTypes.
 Require Import HaskProof.
 Require Import NaturalDeduction.
@@ -199,6 +200,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 +916,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").