diff options
| author | Pierre-Marie Pédrot | 2017-03-20 08:48:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-23 16:33:26 +0100 |
| commit | 91dbe4af7b2a435142dcf40902082f90f07cc8be (patch) | |
| tree | aaae79d684fa71882f9dd4ad1c7a592b29c0cbff /kernel/term_typing.ml | |
| parent | ee1546dc6686e888cc8da5f9442bcf788544dd0e (diff) | |
Documenting the API of side-effects.
Diffstat (limited to 'kernel/term_typing.ml')
0 files changed, 0 insertions, 0 deletions