diff options
| author | Hugo Herbelin | 2018-06-27 13:45:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 10:41:05 +0200 |
| commit | 9371ab87e8bac42216f882ed8f00e6fba9dc6eb0 (patch) | |
| tree | f6ff5b0caa03845548f1ed167eb61d9d3f782f15 /_CoqProject | |
| parent | c2336868843bfe0c8e8a0b669641ca09814a45df (diff) | |
Fixing ltac names interpretation in internals of pattern-matching compilation.
The parts of pattern-matching compilation which generated names may
generate names which collided with names of the Ltac environment.
We fix it by avoiding the names of the Ltac environment.
Diffstat (limited to '_CoqProject')
0 files changed, 0 insertions, 0 deletions