diff options
| author | Tanaka Akira | 2019-02-08 12:52:36 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-08 12:52:36 +0900 |
| commit | 7532f36176c2644bd9167c95fcd33ef3eff631af (patch) | |
| tree | e5cac31106e4fdda872b207088aeac850f554a2b /kernel/nativecode.mli | |
| parent | 613b9ee88067392b7681ee5f0c28d5c5cfff6276 (diff) | |
Change the index "p" to "s" in "type of branches".
In the description of destuctors,
"Type of branches" section uses "p" as the number of arguments.
It is confusing because "p" is used as the number of parameters.
After the section, "Typing rule." section uses "s" without definition as
I q1...qr t1...ts.
It seems that it is the number of arguments.
So, I changed "p" to "s".
"s" is also confusing with sorts, though.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions