diff options
| author | Hugo Herbelin | 2015-05-13 09:11:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-13 09:56:04 +0200 |
| commit | 574b4096517b4ac9189c2226e1cd75745e788db0 (patch) | |
| tree | 704c3c3f4f21fe2ca94e0929eb93c7d99e317512 /kernel/nativecode.ml | |
| parent | d17090cee488844fddc444fdba4fd195c27707c7 (diff) | |
Better fixing #4198 such that the term to match is looked for before
the predicate, thus respecting the visual left-to-right top-down order
(see a45bd5981092).
This fixes CFGV.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions