diff options
| author | Pierre-Marie Pédrot | 2020-12-10 17:33:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-12 14:27:30 +0100 |
| commit | b7ec355d3af240519cde9660dd2562b93f87c555 (patch) | |
| tree | d1206321761c1566c56f49f6aac530e782abbd87 /kernel/type_errors.mli | |
| parent | 233629e8f6e40057a8caf7502047995427740ae8 (diff) | |
Generalize the type of red_expr w.r.t. the type of flags they contain.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions