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

feat(library/tactic): improve error localization when compiling tactics

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-02 12:21:02 -08:00
parent ededf4fc6c
commit fdb169b8f3
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/expr_to_tactic.cpp
View file

@ -171,7 +171,7 @@ static bool is_builtin_tactic(expr const & v) {
} }
tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) { tactic expr_to_tactic(type_checker & tc, elaborate_fn const & fn, expr e, pos_info_provider const * p) {
e = tc.whnf(e).first; e = copy_tag(e, tc.whnf(e).first);
expr f = get_app_fn(e); expr f = get_app_fn(e);
if (!is_constant(f)) if (!is_constant(f))
throw_failed(e); throw_failed(e);