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

fix(library/tactic/smt/smt_state): forgot to set zeta option

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-13 13:33:47 -08:00
parent b305130ec3
commit db646dda89
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/tactic/smt/smt_state.cpp
View file

@ -282,6 +282,7 @@ static expr intros(environment const & env, options const & opts, metavar_contex
The nested instances of has_add and has_zero must be canonized and registered at dcs.
*/
dsimplify_fn dsimp = mk_dsimp(ctx, dcs, s_goal.get_pre_config());
type_context::zeta_scope _1(ctx, s_goal.get_pre_config().m_zeta);
expr target = decl->get_type();
type_context::tmp_locals locals(ctx);
buffer<expr> new_Hs;