diff options
| author | Matthieu Sozeau | 2016-01-12 17:02:09 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-01-12 17:28:04 +0100 |
| commit | 4841b790bbe517deefac11e8df1a7a1494d56bec (patch) | |
| tree | 66f0618b7e63dfd4d6970faf19ebe441ba1e5fb9 /kernel/nativelib.ml | |
| parent | 94b3068c688b289ec26005d13251fc1c3dae6998 (diff) | |
Fix essential bug in new Keyed Unification mode reported by R. Krebbers.
[rewrite] was calling find_suterm using the wrong unification flags, not
allowing full delta in unification of terms with the right keys as desired.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions