diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-01 15:59:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-01 16:01:54 +0200 |
| commit | a4d454beaafd030a5564a395d380748cf90e1b75 (patch) | |
| tree | ca19efa9da4c6c811c9787789b16b21abe4b2cc5 /tactics/taccoerce.mli | |
| parent | 14e6dc5800a28d49dcdb714b06c02fced7b9fdaf (diff) | |
In evarconv, do first-order unification of LetIn's properly, ensuring we compare bodies
of convertible types! Bug found by B. Ziliani.
Diffstat (limited to 'tactics/taccoerce.mli')
0 files changed, 0 insertions, 0 deletions