diff options
| -rw-r--r-- | compiler/coreSyn/CoreLint.lhs | 1 | ||||
| -rw-r--r-- | docs/core-spec/CoreLint.ott | 6 | ||||
| -rw-r--r-- | docs/core-spec/core-spec.pdf | bin | 359837 -> 335916 bytes |
3 files changed, 5 insertions, 2 deletions
diff --git a/compiler/coreSyn/CoreLint.lhs b/compiler/coreSyn/CoreLint.lhs index 5befacdd45..68aaea5b5c 100644 --- a/compiler/coreSyn/CoreLint.lhs +++ b/compiler/coreSyn/CoreLint.lhs @@ -401,7 +401,6 @@ lintCoreExpr (Type ty) lintCoreExpr (Coercion co) = do { (_kind, ty1, ty2, role) <- lintInCo co - ; checkRole co Nominal role ; return (mkCoercionType role ty1 ty2) } \end{code} diff --git a/docs/core-spec/CoreLint.ott b/docs/core-spec/CoreLint.ott index c2dba49612..f2799841dc 100644 --- a/docs/core-spec/CoreLint.ott +++ b/docs/core-spec/CoreLint.ott @@ -122,9 +122,13 @@ G |-ty t : k2 G |-tm case e as z_s return t of </ alti // i /> : t G |-co g : t1 ~Nom k t2 --------------------- :: Coercion +-------------------- :: CoercionNom G |-tm g : t1 ~#k t2 +G |-co g : t1 ~Rep k t2 +----------------------- :: CoercionRep +G |-tm g : (~R#) k t1 t2 + defn G |- name n ok :: :: lintSingleBinding_lintBinder :: 'Name_' {{ com Name consistency check, \coderef{coreSyn/CoreLint.lhs}{lintSingleBinding\#lintBinder} }} {{ tex [[G]] \labeledjudge{n} [[n]] [[ok]] }} diff --git a/docs/core-spec/core-spec.pdf b/docs/core-spec/core-spec.pdf Binary files differindex cb21286abb..4e4ca924fb 100644 --- a/docs/core-spec/core-spec.pdf +++ b/docs/core-spec/core-spec.pdf |