max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/preprocess): do not unfold proofs

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-13 08:46:20 -07:00
parent 4a85c8c145
commit 2ac2badd58
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/preprocess.cpp
View file

@ -91,7 +91,7 @@ class expand_aux_fn : public compiler_step_visitor {
virtual expr visit_app(expr const & e) override {
switch (get_recursor_app_kind(e)) {
case recursor_kind::NotRecursor: {
if (is_not_vm_function(e)) {
if (is_not_vm_function(e) && !ctx().is_proof(e)) {
if (auto r = unfold_term(env(), e)) {
return visit(*r);
}