diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-09 14:41:14 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-09 15:38:50 +0200 |
| commit | 5ea2539d4a7d12938787a74a12112e76aaf2a4ee (patch) | |
| tree | 61251dedf89cf7cfbf3dea06d8853fcc2f43716a /library/library.ml | |
| parent | c2a9cf2730e5e2d7296449ad0acb406e25aead7f (diff) | |
Fixing #4644 (regression of unification on evar-evar problems with a match).
Typically, a problem of the form "?x args = match ?y with ... end" was
a failure even if miller-unification was applicable.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions