abstract out the kind of environment classifiers (ECKind)

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

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index 3539e95..2200f51 100644 (file)
--- 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"