diff options
| author | Pierre-Marie Pédrot | 2020-06-16 14:40:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-23 08:51:47 +0200 |
| commit | 189f4182d6e65ada8fb5856b195b52d15bebdf3a (patch) | |
| tree | e4fccf812ccf27f4d74139a55db61812ad0ce364 /kernel/cbytecodes.ml | |
| parent | 213999187d506394945a4d2163802b504be0c6ac (diff) | |
Use the unification result for eauto's eapply.
Instead of dropping the unification result and calling simple eapply with
the original term, we simply use the same code path as auto and typeclass
eauto, i.e. reuse the clenv for refinement.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions