diff options
| author | Gaëtan Gilbert | 2017-06-13 22:16:46 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-06-13 22:25:36 +0200 |
| commit | 839e87fffdf2634b841aeba6de6d36a2d7a27dbd (patch) | |
| tree | 1303c6797704aa98c38bc140c7ff9bc44b404cfe /engine | |
| parent | 25462addaf604ff51e886bbc92937bb272982b04 (diff) | |
Remove some useless code in Term_typing
The [let _typ = ...] comes from before universe polymorphism. In those
times it was [let _typ, cst = ...] which produced something of use.
The asserts come from 359e4ffe3 and before (2006 and before). In those
times [Typeops.infer] rebuilt the term being typed, but nowadays the
assert seems of little use.
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions