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 /kernel/vmvalues.ml | |
| 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 'kernel/vmvalues.ml')
0 files changed, 0 insertions, 0 deletions