diff options
| author | Vincent Laporte | 2019-02-14 11:17:35 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-02-18 08:19:23 +0000 |
| commit | 647c16764a497b922cc524ba4d956896caa5db5b (patch) | |
| tree | e0a97f1a3b86c21738e28bd88d4bc40016cb1e0f /pretyping/typeclasses_errors.mli | |
| parent | a49077ef67b8e70696ecacc311fc3070d1b7b461 (diff) | |
[Namegen] Use Global.exists_objlabel in `next_global_ident_away`
Fixes #9323.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions