diff options
| author | Gaëtan Gilbert | 2020-04-06 14:40:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 23:10:03 +0200 |
| commit | 988e195c2cd0d97b664193bf1c83c3da2b380f7c (patch) | |
| tree | b8d5aeee1f08b0d61d418cb51448cd506e14296d /kernel/declareops.ml | |
| parent | 8ba8c68eeb8653896523b4bce9453f832c919899 (diff) | |
Checker: factorize handling of typing flags
Diffstat (limited to 'kernel/declareops.ml')
0 files changed, 0 insertions, 0 deletions