diff options
| author | Pierre-Marie Pédrot | 2015-12-01 19:45:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-15 13:12:13 +0100 |
| commit | 968dfdb15cc11d48783017b2a91147b25c854ad6 (patch) | |
| tree | d619d1ebe51d29e5517c9c0385dc4aefe546edbe /kernel/type_errors.mli | |
| parent | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (diff) | |
Monotonizing the Evarutil module.
Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions