diff options
| author | Pierre-Marie Pédrot | 2015-02-27 20:26:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-27 20:31:40 +0100 |
| commit | 64a139406409084f25d3ce35e0fa71bbccc63a20 (patch) | |
| tree | 06906e4576c86e0cc7cb13fe7d04e7184ab84cd1 /plugins | |
| parent | 9f09cbfe36c38a97644ea98c5497636fe74d98d6 (diff) | |
Fixing bug #3249.
Instead of substituting carelessly the recursive names in Ltac interpretation,
we declare them in the environment beforehand, so that they get globalized
as themselves. We restore the environment afterwards by transactifying the
globalization procedure.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions