diff options
| author | Théo Zimmermann | 2018-05-27 12:31:22 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-27 14:31:34 +0200 |
| commit | efe0768adcbe1409311136796e1dc350d57061b4 (patch) | |
| tree | eb6fe6b9e24ef3a7c1f77b3098e56bce62ee291c /kernel/nativelambda.ml | |
| parent | 9cf5d8dbfc6046adf92ba461b5a0a697fd578955 (diff) | |
Document Variant properly.
Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121
This commit also marginally improves the Record doc (a lot more remains to do).
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions