aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorherbelin2010-11-07 23:35:56 +0000
committerherbelin2010-11-07 23:35:56 +0000
commitd46ed1de8e9c928eed1121ae77bd308ecb88205b (patch)
tree9ee1240ccae3c67631997a4299a4e9c80f78473f /kernel
parent966a0d7534763c65e65d32b5d6223fd34cfa2445 (diff)
Delayed the evar normalization in error messages to the last minute
before the message is delivered to the user. Should avoid useless computation in heavily backtracking tactics (auto, try, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions