diff options
| author | Hugo Herbelin | 2015-10-01 09:29:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-02 17:42:04 +0200 |
| commit | 9227d6e9412ae4ebe70fb9b6bd5d2f6ecc354864 (patch) | |
| tree | 8320e277f3d76fc1deb98e7671b0554446000dba /dev/doc | |
| parent | 6e1c88226eb2ab188a1aaaf9a31667967c85fc65 (diff) | |
Improving reference manual in that auto uses simple apply rather than apply.
Still, there are small differences, e.g. on
"use_metas_eagerly_in_conv_on_closed_terms", but also maybe in some
amount of use of delta that Matthieu would know better than me if it
matters or not in practice.
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions