summaryrefslogtreecommitdiff
path: root/docs/core-spec/CoreLint.ott
diff options
context:
space:
mode:
Diffstat (limited to 'docs/core-spec/CoreLint.ott')
-rw-r--r--docs/core-spec/CoreLint.ott2
1 files changed, 0 insertions, 2 deletions
diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott
index 22949eddf3..b142901ede 100644
--- a/docs/core-spec/CoreLint.ott
+++ b/docs/core-spec/CoreLint.ott
@@ -115,8 +115,6 @@ G |-ty t : k2
---------------------------------------------------- :: Case
G |-tm case e as z_s return t of </ alti // i /> : t
-% Type case of lintCoreExpr omitted because it is irrelevant
-
G |-co g : t1 ~#k t2
-------------------- :: Coercion
G |-tm g : t1 ~#k t2