diff options
| author | Hugo Herbelin | 2020-08-19 03:38:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-19 20:35:28 +0200 |
| commit | f10b2021cce7bca2d0234e9ab73be47cdc3bf6fc (patch) | |
| tree | e6210ef23293e87928eacdfa5e5b3d8ff7d3fe64 /engine | |
| parent | 9029403db62163924a329acad3fbdb180cdc1d7a (diff) | |
Yet other tactic error location fixes (see PR#12223 and PR#12774).
When calling an Ltac function, add specific locations when
interpreting the function, when interpreting the arguments and when
executating the call (in a TacArg).
Diffstat (limited to 'engine')
0 files changed, 0 insertions, 0 deletions