diff options
| author | Gaëtan Gilbert | 2020-03-30 13:04:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-03-30 13:04:47 +0200 |
| commit | e21aae1b32adba4e8673783f327826d279e05ced (patch) | |
| tree | d20413576f188f661914d38279f8b7d592186b95 /kernel/type_errors.ml | |
| parent | 7ff44dd02d935cb078487629b342b7106cc72955 (diff) | |
| parent | f0ef2d764673670fef52873c441bbbb2f1f7a34d (diff) | |
Merge PR #11951: Remove a useless reversed variant in Vars.
Reviewed-by: SkySkimmer
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions