diff options
| author | Gaëtan Gilbert | 2020-08-24 13:32:59 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-25 16:15:18 +0200 |
| commit | a9a0307e2695e97143a8fc36ccdbfdd7de0c3820 (patch) | |
| tree | 81e8425eaffc9cc49a1f1944b501970b2319ba63 /kernel/type_errors.mli | |
| parent | 2eac36b65732e0302f04693a4524c454fcbb5760 (diff) | |
omega: stop using intro_using
This makes the test suite Omega.v compatible with Mangle Names
Not sure how `reintroduce` works since it ignores the refreshed name,
considering omega is deprecated it's not worth figuring out so long as
it works (NB making it use intro_mustbe_force makes the test suite
fail so it must be doing something right).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions