diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-21 11:37:06 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2015-12-22 16:25:20 +0100 |
| commit | e1ac3467db26f9bcc09f12989eeb8379c4fc5817 (patch) | |
| tree | e9c46f9944c414cda11513188903839131b9c582 /library/global.mli | |
| parent | b88929d9d8de179a7e356cf9cbe2afef76f905a3 (diff) | |
COMMENTS: added to the "Names.inductive" and "Names.constructor" types.
Diffstat (limited to 'library/global.mli')
0 files changed, 0 insertions, 0 deletions