From 7f496f43f15e691ed79c63597f7fef6eb040be6c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Sep 2018 18:26:23 -0700 Subject: [PATCH] fix(library/compiler/lcnf): it was not erasing proofs that start with `Pi` --- src/library/compiler/lcnf.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 7c8b9ac8fa..2585640a1f 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -464,16 +464,16 @@ public: if (is_sort(type)) { // Types are not pre-processed return cache_result(e, e, shared); + } else if (tc.is_prop(type)) { + // We replace proofs using `lc_proof` constant + expr r = mk_app(mk_constant(get_lc_proof_name()), type); + return cache_result(e, r, shared); } else if (is_pi(type)) { // Functions that return types are not pre-processed while (is_pi(type)) type = binding_body(type); if (is_sort(type)) return cache_result(e, e, shared); - } else if (tc.is_prop(type)) { - // We replace proofs using `lc_proof` constant - expr r = mk_app(mk_constant(get_lc_proof_name()), type); - return cache_result(e, r, shared); } }