diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index b94286f19e..757f10fb4b 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -686,13 +686,13 @@ where decls.forM fun decl => visit decl.value def instantiateRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr := - if !e.hasFVar then + if !e.hasLooseBVars then e else e.instantiateRange beginIdx endIdx (args.map (·.toExpr)) def instantiateRevRangeArgs (e : Expr) (beginIdx endIdx : Nat) (args : Array Arg) : Expr := - if !e.hasFVar then + if !e.hasLooseBVars then e else e.instantiateRevRange beginIdx endIdx (args.map (·.toExpr))