diff options
| author | Pierre-Marie Pédrot | 2015-02-27 14:05:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-27 14:07:15 +0100 |
| commit | 9fea58122001535bdee63317b56f2afb727167c7 (patch) | |
| tree | d78f84e01a6d1c11273abe3e5f86ce9d61dc8ab9 /plugins/syntax | |
| parent | dbdf0648f4588d812a20ea4ba7d3e866f024073c (diff) | |
Somehow fixing bug #3467.
The notations using tactics in term seem now not to respect globalized names.
It is not obvious that this is the expected behaviour, but at least it does
not die with an anomaly.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions