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