From f8caacfcb34bdcaa551fc1391b9767d004e505cd Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 12 Jan 2017 20:54:41 +0100 Subject: [PATCH] fix(tools/super/superposition): use none transparency to remove beta-redex --- library/tools/super/superposition.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/tools/super/superposition.lean b/library/tools/super/superposition.lean index 830b64e80f..6782649cb2 100644 --- a/library/tools/super/superposition.lean +++ b/library/tools/super/superposition.lean @@ -84,7 +84,7 @@ atom_univ ← infer_univ atom, op1 ← qf1.1^.open_constn i1, op2 ← qf2.1^.open_constn c2^.num_lits, hi2 ← (op2.2^.nth i2)^.to_monad, -new_atom ← whnf $ app abs_rwr_ctx rwr_to', +new_atom ← whnf_core transparency.none $ app abs_rwr_ctx rwr_to', new_hi2 ← return $ local_const hi2^.local_uniq_name `H binder_info.default new_atom, new_fin_prf ← return $ app_of_list (const congr_ax [lf_univ, univ, atom_univ]) [c1^.local_false, eq_type, rwr_from, rwr_to,