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 /configure.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 'configure.ml')
0 files changed, 0 insertions, 0 deletions