diff options
| author | Matthieu Sozeau | 2016-05-19 13:03:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 8d06718fd4d99f4e5bc33452a02ea27d5a9279ed (patch) | |
| tree | 5c3a3207ac1af512db69881c86c35e575d73c9a6 /engine/proofview.mli | |
| parent | 1fda28c317a2394aa3ee84e0e680e878333c8782 (diff) | |
typeclass resolution: add two compatibility options
Set Typeclasses Compatibility "8.5". uses the old resolution
tactic (off by default, but useful for debugging incompatibilities)
Set Typeclasses Unification Compatibility "8.5".
uses the old clenv unification tactic in resolution even
with the new proof engine (on by default for now).
Also fix the 8.5-compatible unification with the new engine resolution
function, by using with_shelf and unshelve.
Diffstat (limited to 'engine/proofview.mli')
0 files changed, 0 insertions, 0 deletions