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

feat(library/tactic/simp_lemmas): use proof for refl lemmas at simp_lemma_rewrite too

Browse source 
I forgot to do it at 9fcb3ae4b5
This commit is contained in:
Leonardo de Moura 2017-06-21 16:53:35 -07:00
parent b9dee04fdb
commit 3195a800f4
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/tactic/simp_lemmas.cpp
View file

@ -1395,12 +1395,9 @@ static simp_result simp_lemma_rewrite(type_context & ctx, simp_lemma const & sl,
return simp_result(e);
}
}
if (sl.is_refl()) {
return simp_result(new_rhs);
} else {
expr pf = ctx.instantiate_mvars(sl.get_proof());
return simp_result(new_rhs, pf);
}
expr pf = ctx.instantiate_mvars(sl.get_proof());
return simp_result(new_rhs, pf);
}
vm_obj simp_lemmas_rewrite_core(transparency_mode const & m, simp_lemmas const & sls, vm_obj const & prove_fn,