diff options
| author | Hugo Herbelin | 2016-06-18 11:18:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-18 11:18:01 +0200 |
| commit | c064fb933a16dc25b8172a1a2e758f538ee7285e (patch) | |
| tree | 1dcb78fe37b19a4d063a1ef2ba7bfba2135e40bc /plugins/syntax/nat_syntax_plugin.mlpack | |
| parent | 5401deb474ca596ffbb23a12f4b70e6def1d0d65 (diff) | |
A hack to fix another regression with Ltac trace report in 8.5. E.g.
Goal 0=0 -> true=true.
intro H; rewrite H1.
was highlighting H1 but
Goal 0=0 -> true=true.
intro H; rewrite H.
was only highlighting the whole "intro H; rewrite H".
Diffstat (limited to 'plugins/syntax/nat_syntax_plugin.mlpack')
0 files changed, 0 insertions, 0 deletions