summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorPeter Sewell2017-02-25 17:01:06 +0000
committerPeter Sewell2017-02-25 17:01:06 +0000
commit95f6c0b034eef25fe2a1cfb5654fc9a07956a0fc (patch)
treea8a18d6ed611a9e5e8e096a7cd5ec33ad95193a5
parentdc61eded5d3b0a547a64e4a89343aa1d8eafa713 (diff)
wib
-rw-r--r--language/l2.ott2
1 files changed, 1 insertions, 1 deletions
diff --git a/language/l2.ott b/language/l2.ott
index 74431b32..4a0d138e 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -135,7 +135,7 @@ id :: '' ::=
% targets use alphabetical infix operators.
kid :: '' ::=
- {{ com [[Type]], [[Nat]], [[Order]], and [[Effect]] variables }}
+ {{ com kinded IDs: [[Type]], [[Nat]], [[Order]], and [[Effect]] variables }}
{{ aux _ l }}
| ' x :: :: var