diff options
| author | Maxime Dénès | 2016-07-04 15:02:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-04 15:03:31 +0200 |
| commit | 0eb08b70f0c576e58912c1fc3ef74f387ad465be (patch) | |
| tree | 9cbd5c2ebd6760293f4cea54c899492007c05215 /kernel/nativecode.mli | |
| parent | 2ce64cc3124d30dbd42324c345cec378ccd66106 (diff) | |
Revert "Improve the interpretation scope of arguments of an ltac match."
We apply this patch to trunk for integration in 8.6 instead.
This reverts commit 715f547816addf3e2e9dc288327fcbcee8c6d47f.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions