abstract out the kind of environment classifiers (ECKind)

[coq-hetmet.git] / src / ExtractionMain.v

diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v
index 58bc13e..e628f26 100644 (file)
--- 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_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).
 
       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).
       fun TV ite => TApp (TApp (TApp (@TyFunApp TV 
         hetmet_PGArrowTyCon
         nil _ TyFunApp_nil) (a TV ite)) (b TV ite)) (c TV ite).