diff options
| author | Tanaka Akira | 2019-02-10 22:57:13 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-10 22:57:13 +0900 |
| commit | 4a5eb765f7c1a5795368c7cdcd2a6d85eef20256 (patch) | |
| tree | d9ac1efcc509f675460fec6b4e124946fc7e7d2a /kernel/type_errors.ml | |
| parent | 283046a15dc5e4cd8877df44321dd8020de7bca6 (diff) | |
Change "I" to "I_p".
Since the type of "c" is "I_p ...", the constructor should
return the value of it.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions