X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FExtractionMain.v;h=e628f268153b1602c975584a4820bb5c2be96ac1;hp=58bc13e2ce945e7ecbd850cf911937fdca5ba7fa;hb=b4857a6f575dffd5c9c9d5decbc21ff63a338270;hpb=cb424978e057bc2b4868517302738d52246fba04

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 58bc13e..e628f26 100644
--- a/src/ExtractionMain.v
+++ b/src/ExtractionMain.v
@@ -335,13 +335,13 @@ Section core2proof.
     Definition ga_unit TV : RawHaskType TV ★ := @TyFunApp TV UnitTyCon nil         ★ TyFunApp_nil.
     Definition ga_prod TV (a b:RawHaskType TV ★) : RawHaskType TV ★  :=
       TApp (TApp (@TyFunApp TV PairTyCon nil _ TyFunApp_nil) a) b.
-    Definition ga_type {TV}(a b c:RawHaskType TV ★) : RawHaskType TV ★ :=
+    Definition ga_type {TV}(a:RawHaskType TV ECKind)(b c:RawHaskType TV ★) : RawHaskType TV ★ :=
       TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) a) b) c.
     Definition ga := @ga_mk ga_unit ga_prod (@ga_type).
 
-    Definition ga_type' {Γ}(a b c:HaskType Γ ★) : HaskType Γ ★ :=
+    Definition ga_type' {Γ}(a:HaskType Γ ECKind)(b c:HaskType Γ ★) : HaskType Γ ★ :=
       fun TV ite => TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).