diff options
| author | Pierre-Marie Pédrot | 2016-08-19 20:36:32 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-08-19 20:38:21 +0200 |
| commit | 553f92462a2bc5e45a0d05c5b051fe51f2e7f2c0 (patch) | |
| tree | 016a04ae966f698cefb4c183ec72ad36f87a3e16 /kernel/type_errors.mli | |
| parent | 82dc377451e2dc7810eea136b9a6ab8fc5ae48b5 (diff) | |
Fix performance bug: do not compute implicits of abstracted lemmas.
This was showing up in some of Jason's examples, where an abstract had to
compute the weak head form of a huge term in order to find the corresponding
implicit arguments.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions