From e81673366a6a6eeef98a2656423fd1173d7459bf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 9 Oct 2022 11:55:30 -0700 Subject: [PATCH] chore: remove leftover --- src/Lean/Compiler/LCNF/ToLCNF.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 0b4b5080cb..84fe803763 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -504,7 +504,6 @@ where ps ← ps.mapM fun p => do let type ← inferType p.toExpr if (← isTypeFormerType type) then - trace[Meta.debug] "{p.binderName} is type former" modify fun s => { s with toAny := s.toAny.insert p.fvarId } /- Recall that we may have dependent fields. Example: