diff options
| author | Clément Pit-Claudel | 2019-05-23 14:47:54 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-23 14:47:54 -0400 |
| commit | ad6e002b2d938217edb55da027ae380a6e4eff92 (patch) | |
| tree | d2cc7c400723aac8db62baadea4ef9f82d40831f /pretyping/typeclasses.ml | |
| parent | 2f5a1a2d846e65b7e6bcf76ab374b0290662a27f (diff) | |
| parent | 28bf625cbac7dcf4a21907674b5bd30eb53e5e87 (diff) | |
Merge PR #10217: Less undefined tokens
Ack-by: JasonGross
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
Diffstat (limited to 'pretyping/typeclasses.ml')
0 files changed, 0 insertions, 0 deletions