diff options
| author | Pierre-Marie Pédrot | 2020-06-24 22:43:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-05 21:41:08 +0200 |
| commit | 9895f45b4895a321fc946eb64c17b1db5a78cda9 (patch) | |
| tree | cfdcb17f9eb22b091af5f5de5e70fa6d33c34c91 /pretyping/typeclasses_errors.ml | |
| parent | a659a12ca88bebaf1fa7f201023cc06be34849d9 (diff) | |
Inline make_elim_fun in Tacred.
We seize the opportunity to simplify the code and hoist out computations
that can be avoided.
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions