X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;h=d575d12da0d535351ff97076143bdc5b073ae7b0;hp=2200f517165589a3c832dba14e2d1cf205aec3cf;hb=64a5591df2cf9e7fde9fbd8ef7ea712bf28df201;hpb=b4857a6f575dffd5c9c9d5decbc21ff63a338270

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 2200f51..d575d12 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -38,7 +38,7 @@ Notation "'★'"   := KindStar.
 Notation "a ⇛ b" := (KindArrow a b).
 
 (* the kind of environment classifiers *)
-Definition ECKind := ★ .  
+Definition ECKind := ★ ⇛ ★ ⇛ ★.  
 Opaque ECKind.
 
 Fixpoint kindToLatexMath (k:Kind) : LatexMath :=