diff options
| author | Hugo Herbelin | 2020-11-29 09:40:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2021-01-18 15:42:00 +0100 |
| commit | eb38680520811e7a5e64678719d7b57e87af1269 (patch) | |
| tree | 1caae5f8e985f546a65c5bba5d16ce2247eda33f /pretyping/typeclasses_errors.ml | |
| parent | 53e287871e2d03f95e754ffa58047668799e54ee (diff) | |
Preventing internal temporary names to impact the "?H"-like intro-pattern names.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions