diff options
| author | Hugo Herbelin | 2020-11-28 15:10:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2021-01-18 15:25:26 +0100 |
| commit | e56c65cf68c4055b4e1272b5a2afbf5803d93a42 (patch) | |
| tree | 8ad85144180f8bd359afe078f846b66b8472e7c3 /pretyping/typeclasses_errors.ml | |
| parent | f44e65e0d209fdada20998d661ad10a5e82a0d92 (diff) | |
Fixes #13413: freshness issue with "%" introduction pattern.
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions