diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-14 15:56:16 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-14 16:02:02 +0200 |
| commit | c69404402212ed9d541899ae78ac889e62cf238a (patch) | |
| tree | 11f313c9b5ddb0c61c2250cf305fe9d6e717a008 /proofs/refiner.ml | |
| parent | cd98815d0e1e57eed3e19eb9516a980b82c60a36 (diff) | |
Remove confusing behavior of unify_with_subterm that could fail with
NoOccurenceFound when only typeclass resolution failed. Might break
some scripts relying on backtracking on typeclass resolution failures
to find other terms to rewrite, which can be fixed using occurrences
or directly setoid_rewrite.
Diffstat (limited to 'proofs/refiner.ml')
0 files changed, 0 insertions, 0 deletions