diff options
| author | Anton Trunov | 2018-02-13 22:55:01 +0100 |
|---|---|---|
| committer | Anton Trunov | 2018-03-04 19:24:19 +0100 |
| commit | 5233abd2f876af6b9e5b705b2ab4df8cdb50b12e (patch) | |
| tree | dc071d2007b80eeaeb33b2b7b8b45fb70b197c8b /pretyping/typeclasses_errors.ml | |
| parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) | |
ssr: fix typo in doc comment
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions