diff options
| author | Gaëtan Gilbert | 2019-12-30 11:30:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-14 14:56:03 +0100 |
| commit | e4ebe14337743eba09b93c6f5bff1e1d78083741 (patch) | |
| tree | 11463c41539dd6a1af8d3c989a90892c4bc8193d /kernel/indtypes.mli | |
| parent | 8b4f78ded7269139c7e9c222c6382a788c48039a (diff) | |
infercumulativity: take less arguments
Diffstat (limited to 'kernel/indtypes.mli')
0 files changed, 0 insertions, 0 deletions