summaryrefslogtreecommitdiff
path: root/language
diff options
context:
space:
mode:
Diffstat (limited to 'language')
-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