diff options
| author | Maxime Dénès | 2016-07-04 16:18:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 16:18:06 +0200 |
| commit | da99355b4d6de31aec5a660f7afe100190a8e683 (patch) | |
| tree | 3b00f4b967ad27eb90518627948275fb0b7b72d2 /kernel/nativecode.ml | |
| parent | c78b84425be7535e46c63e80200c07a1921e67bd (diff) | |
Revert "Revert "Improve the interpretation scope of arguments of an ltac match.""
We apply this patch to trunk so that it is integrated in 8.6.
This reverts commit 0eb08b70f0c576e58912c1fc3ef74f387ad465be.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions