fix(library/elaborator): missing normalization step for semantic attachments

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-28 07:42:14 -07:00
parent 4564bfa1d3
commit b16a64f44b

View file

@ -529,6 +529,10 @@ class elaborator::imp {
} }
} }
} }
if (to_value(f).normalize(new_args.size(), new_args.data(), r)) {
a = r;
return;
}
if (modified) { if (modified) {
a = mk_app(new_args); a = mk_app(new_args);
return; return;