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

fix(library/unifier): remove incorrect assertion

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-26 07:52:10 -07:00
parent c1b523d642
commit 556861c8d6
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/unifier.cpp
View file

@ -1199,7 +1199,6 @@ struct unifier_fn {
*/ */
void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j, void mk_simple_nonlocal_projection(expr const & m, buffer<expr> const & margs, unsigned i, expr const & rhs, justification const & j,
buffer<constraints> & alts) { buffer<constraints> & alts) {
lean_assert(!is_local(rhs));
expr const & mtype = mlocal_type(m); expr const & mtype = mlocal_type(m);
unsigned vidx = margs.size() - i - 1; unsigned vidx = margs.size() - i - 1;
expr const & marg = margs[i]; expr const & marg = margs[i];