diff options
| author | Hugo Herbelin | 2020-07-14 16:02:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-15 21:07:59 +0100 |
| commit | 60d15dc5f56411c53f6974c4df900b4ce59da23f (patch) | |
| tree | 590caddbba31046ec6790bb473aa74a897624415 /kernel/nativecode.ml | |
| parent | 3ac39cdd88368c62aa25eaa37fb61fb16406e180 (diff) | |
Fixing Locate for recursive notations with names.
E.g. Locate "(x , y , .. , z )" now works while only
Locate "(_ , _ , .. , _ )" was working before.
This also fixes a confusion between a variable and its anonymization
into _, wrongly finding notations mentioning '_'.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions