diff options
| author | Hugo Herbelin | 2015-09-08 17:46:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-08 17:57:41 +0200 |
| commit | 703e5b595a4a96dc9ff3df7ad10f90a238a061b6 (patch) | |
| tree | 3176639ec6459f20f221791e71d1c9bbfeee8a81 /kernel/nativevalues.ml | |
| parent | 7e00e8d602e67810700a7071c419ffd7ef8806c5 (diff) | |
Emphasizing that eta for vectors is an instance of caseS, as pointed
out to me by Pierre B.
Also extending use of bullets in Vectors where relevant.
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions