diff options
| author | Hugo Herbelin | 2015-12-10 12:22:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-15 11:58:21 +0100 |
| commit | 78896394b49b0d8b89c81378f9437e69a86b6363 (patch) | |
| tree | 3c28f3a2c416d32c23c654cbba68f911dbc4b731 /kernel/type_errors.ml | |
| parent | 1aecaf88e5491d29b200515fc64ce3d479318758 (diff) | |
Granting clear_flag in injection, even legacy mode. This is possible
since the clear_flag is new.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions