From adcfd896235cf00237d283ad52505b8de9e0d3b8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 17 Sep 2016 18:29:11 -0700 Subject: [PATCH] feat(library/type_context): remove normalize --- src/library/type_context.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index c94bda1d35..f178c0ac57 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1225,8 +1225,8 @@ bool type_context::is_def_eq_core(level const & l1, level const & l2) { } } - level new_l1 = normalize(instantiate_mvars(l1)); - level new_l2 = normalize(instantiate_mvars(l2)); + level new_l1 = instantiate_mvars(l1); + level new_l2 = instantiate_mvars(l2); if (l1 != new_l1 || l2 != new_l2) return is_def_eq_core(new_l1, new_l2);