diff options
| author | Arnaud Spiwack | 2014-09-15 14:42:05 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-15 15:44:11 +0200 |
| commit | 7ec7714aa7649fc1bae463f4200fa8c16729026a (patch) | |
| tree | 4da4fc06959bd438ae4c6aa111a7176611865628 /interp/implicit_quantifiers.ml | |
| parent | 006c487f8af220cf8a374bc38d06c3d58fe4335b (diff) | |
Fix: when interpreting a identifier in pretying, use the Ltac identifier substitution at the right place.
I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
0 files changed, 0 insertions, 0 deletions