From cda867b1245b4819d72097bfbb5560cb72ed9765 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 Jul 2016 17:22:37 -0700 Subject: [PATCH] fix(library/defeq_canonizer): bugs found by Daniel This is a cleanup of https://github.com/leanprover/lean/pull/1081/commits/10d23f0075b9d6607ab5a7528a9b3ba4466dd99e --- src/library/defeq_canonizer.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/defeq_canonizer.cpp b/src/library/defeq_canonizer.cpp index 349e05c46e..d7bbc75904 100644 --- a/src/library/defeq_canonizer.cpp +++ b/src/library/defeq_canonizer.cpp @@ -15,7 +15,7 @@ struct defeq_canonize_cache { environment m_env; /* Canonical mapping I -> J (i.e., J is the canonical expression for I). Invariant: locals_subset(J, I) */ - expr_map m_C; + expr_struct_map m_C; /* Mapping from head symbol N to list of expressions es s.t. for each e in es, head_symbol(e) = N. */ name_map> m_M; @@ -116,6 +116,7 @@ struct defeq_canonize_fn { if (get_weight(e) < get_weight(*new_e) && locals_subset(e, *new_e)) { replace_C(*new_e, e); replace_M(*h, *new_e, e); + insert_C(e, e); return e; } else { insert_C(e, *new_e);