From 2434024272d02f64950f997da8f63cefb5147d85 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2014 15:46:49 -0800 Subject: [PATCH] fix(library/rewriter): warning in release mode Signed-off-by: Leonardo de Moura --- src/library/rewriter/rewriter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp index 0b52602c83..73285591ea 100644 --- a/src/library/rewriter/rewriter.cpp +++ b/src/library/rewriter/rewriter.cpp @@ -53,8 +53,8 @@ pair rewrite_lambda_type(environment const & env, context & ctx, exp expr const & body = abst_body(v); // expr const & pf_ty = result_ty.second; expr const & new_v = mk_lambda(n, new_ty, body); - expr const & ty_ty = ti(ty, ctx); - lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types + // expr const & ty_ty = ti(ty, ctx); + // lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types expr proof; #if 0 // TODO(Leo): we don't have heterogeneous equality anymore = mk_subst_th(ty_ty, ty, new_ty,