diff options
| author | Tanaka Akira | 2019-01-31 19:24:39 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 19:24:39 +0900 |
| commit | 6f53aca07665c45af6c1713869f5434208607188 (patch) | |
| tree | c196798b31246a2b07578f38897f0c5f509e930b /kernel/nativecode.ml | |
| parent | fcb4cf7628ea67cf342f8c39cb7f5151897ff72c (diff) | |
The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.
c can be non-function since c:U.
So, c c' is not typeable.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions