X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;ds=sidebyside;f=src%2FHaskKinds.v;h=3539e953ab946166f39e094c64d0157a5a4281d8;hb=e83fd6f566ed0a7aaff19d67c2c2b64d08f98f7c;hp=b61ed0752aac28ba04e694ac19bbd889d8d90c8f;hpb=97552c1a6dfb32098d4491951929ab1d4aca96a0;p=coq-hetmet.git

diff --git a/src/HaskKinds.v b/src/HaskKinds.v
index b61ed07..3539e95 100644
--- a/src/HaskKinds.v
+++ b/src/HaskKinds.v
@@ -12,7 +12,6 @@ Variable Note                : Type.                         Extract Inlined Con
 Variable natToString         : nat         -> string.        Extract Inlined Constant natToString => "natToString".
 Instance NatToStringInstance : ToString nat := { toString := natToString }.
 
-(* Figure 7: production κ, ι *)
 Inductive Kind : Type := 
   | KindStar          : Kind                      (* ★  - the kind of coercions and the kind of types inhabited by [boxed] values *)
   | KindArrow         : Kind  -> Kind  -> Kind    (* ⇛  - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)