diff options
| author | Gaëtan Gilbert | 2019-01-24 13:18:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-24 13:18:28 +0100 |
| commit | ad227e6b900d15c60133e1997cdaed80358b85c7 (patch) | |
| tree | e17c2b2efc234c0bf49f11930c9d7e3a4004ad37 /kernel/type_errors.ml | |
| parent | f5241b99bb15f019eb629a7f24f2993f011e7e06 (diff) | |
Skip indirection through Evd for obligation ustate manipulation
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions