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

fix(library/tactic/inversion_tactic): incorrect use of optimization

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-20 16:21:44 -07:00
parent 107763a506
commit 431eade894
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/tactic/inversion_tactic.cpp
View file

@ -182,8 +182,8 @@ class inversion_tac {
for (unsigned i = fidx; i < args.size(); i++) { for (unsigned i = fidx; i < args.size(); i++) {
if (!is_local(args[i])) if (!is_local(args[i]))
return false; // the indices must be local constants return false; // the indices must be local constants
for (unsigned j = fidx; j < i; j++) { for (unsigned j = 0; j < i; j++) {
if (mlocal_name(args[j]) == mlocal_name(args[i])) if (is_local(args[j]) && mlocal_name(args[j]) == mlocal_name(args[i]))
return false; // the indices must be distinct local constants return false; // the indices must be distinct local constants
} }
} }