michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic/exact_tactic): do not report unassigned metavariables in the 'refine' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-03 20:39:51 -07:00
parent 87aaf373f4
commit 3c8c75470f
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/tactic/exact_tactic.cpp
View file

@ -33,7 +33,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
return none_proof_state(); return none_proof_state();
} }
expr t = head(gs).get_type(); expr t = head(gs).get_type();
bool report_unassigned = enforce_type_during_elaboration; bool report_unassigned = !allow_metavars && enforce_type_during_elaboration;
optional<expr> new_e; optional<expr> new_e;
try { try {
new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),