diff options
| author | Hugo Herbelin | 2015-10-04 08:14:39 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-06 08:36:05 +0100 |
| commit | fe2776f9e0d355cccb0841495a9843351d340066 (patch) | |
| tree | 416715dd9dbbd9413b0b7010156d82a286b50245 /kernel | |
| parent | 3cd31aaedb729f1d5284e5e3e46151412b78859a (diff) | |
RefMan, ch. 1 and 2: avoiding using the name "constant" when
"constructor" and "inductive" are meant also.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions