X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskKinds.v;h=d575d12da0d535351ff97076143bdc5b073ae7b0;hp=3539e953ab946166f39e094c64d0157a5a4281d8;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=ec8ee5cde986e5b38bcae38cda9e63eba94f1d9f

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 3539e95..d575d12 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -37,6 +37,10 @@ Instance KindToString : ToString Kind := { toString := kindToString }.
 Notation "'★'"   := KindStar.
 Notation "a ⇛ b" := (KindArrow a b).
 
+(* the kind of environment classifiers *)
+Definition ECKind := ★ ⇛ ★ ⇛ ★.  
+Opaque ECKind.
+
 Fixpoint kindToLatexMath (k:Kind) : LatexMath :=
   match k with
   | ★                            => rawLatexMath "\star"