diff options
| author | Théo Zimmermann | 2019-02-25 10:53:57 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-25 10:53:57 +0100 |
| commit | 34dd54baafb68f2efc07701e2b0f8c7b95b12cba (patch) | |
| tree | f0e86c7fd81e17ee2a7e98ca45c6d02f7f98888a /pretyping/typeclasses_errors.ml | |
| parent | c37e90b67c74b32837409a9a424757246067ef1b (diff) | |
| parent | 878fe50b288d52eeda84be386a28fe3c6b029f30 (diff) | |
Merge PR #9511: Enable whitespace checking for some forgotten files.
Reviewed-by: Zimmi48
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions