X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskFlattener.v;h=cd5bd57942075f15e4f00b0aff991c572764c974;hp=47315bb2b265b87f1dc001b8bd8ce69d31193cd7;hb=c5455f79a56b00af66a980cf0469290fa9c62f96;hpb=1215a7fa07083dadaad909ca023a305fc75f7632

diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v
index 47315bb..cd5bd57 100644
--- a/src/HaskFlattener.v
+++ b/src/HaskFlattener.v
@@ -204,8 +204,10 @@ Section HaskFlattener.
   Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
     fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr).
 
-  Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind )(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
-    gaTy TV ec (ga_mk_tree' ec ant) (ga_mk_tree' ec suc).
+  Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ :=
+    gaTy TV ec
+    (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc)))
+    (ga_mk_tree' ec (      mapOptionTree                       drop_arg_types  suc) ).
 
   Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ :=
     fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc).