diff options
| author | Tanaka Akira | 2019-01-31 16:14:38 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:14:38 +0900 |
| commit | a5abe07d98b089808b2a98b4a90f7974eddc52c7 (patch) | |
| tree | a23724981a99a0396e78c68da6992bfae864353c /kernel/type_errors.mli | |
| parent | ddcd0afd740278b7b18999cd8ad4aa01c8b26d5f (diff) | |
Change {\Sort} to \Sort.
After #9435 (Use \mathcal instead of \cal), \Sort doesn't have
font changing effect.
So, {\Sort} is same as \Sort now and the former is changed to latter in
cic.rst.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions