diff options
| author | Hugo Herbelin | 2020-09-09 12:58:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-16 08:08:18 +0200 |
| commit | fc0aa1e70cb1891ef3f62566af4e551d06bfb613 (patch) | |
| tree | bda03cc9cd546c2c7355f9f6ff893bd6612a9e51 /_CoqProject | |
| parent | d6b6e1d6ceadfe65ea398786361ff7737624deaf (diff) | |
More improvements in locating tactic errors.
We finally pass the location in the "ist", and keep it in the "VFun"
which is associated to expanded Ltac constants.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions