diff options
author | 2014-09-18 21:39:03 +0200 | |
---|---|---|
committer | 2014-09-18 21:39:03 +0200 | |
commit | 23041481ff368b0b4cfc9a2493c9f465df90ea90 (patch) | |
tree | fa981847c7fe17b18d4453403d19df9e32b26a38 /doc/tools | |
parent | dbdff037af1a80d223be6e4d093417bae301c583 (diff) |
Fix debug printing with primitive projections.
Add a flag to indicate if we're in the toplevel or debuggger to not try
to retype terms in the wrong environment (and making find_rectype,
get_type_of untraceable). This fixes bug #3638 along with the previous
commit.
Diffstat (limited to 'doc/tools')
0 files changed, 0 insertions, 0 deletions