diff options
| author | Hugo Herbelin | 2015-11-25 17:33:24 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-25 17:35:43 +0100 |
| commit | e92aeed3abcf7d42045deb9fb3a450d3527eadc9 (patch) | |
| tree | 7609b2a7c330394819f8f8f9d7d176983638dbd8 /lib | |
| parent | 6f9cc3aca5bb0e5684268a7283796a9272ed5f9d (diff) | |
Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej).
This was not a typo (was correctly taking the family type of the type).
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions