diff options
| author | Gaëtan Gilbert | 2020-09-30 12:50:37 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-06 12:40:35 +0200 |
| commit | 07b7bd7f8358d199b0464a673aec50dedae0a45d (patch) | |
| tree | d3027890b209f842fc9b0321ceea664399a9467c /pretyping/typeclasses.mli | |
| parent | 661d84228fa1a6750b4a80f41c3e012e6de763bf (diff) | |
Implicit_quantifiers don't use precomputed is_class data
Fix #13117
We alternatively could fix the generation of the data with Existing
Class but I prefer moving towards removing it.
Diffstat (limited to 'pretyping/typeclasses.mli')
0 files changed, 0 insertions, 0 deletions