From 8088145da8b268bf3ef7e80ecb3c3a25e9647fce Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 10 Dec 2020 17:15:43 +0100
Subject: [PATCH] chore: remove obsolete code

---
 src/Lean/Compiler/IR/Checker.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 6a60d3dd11..0b55cd354f 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -82,8 +82,6 @@ def checkScalarVar (x : VarId) : M Unit :=
   checkVarType x IRType.isScalar
 
 def checkFullApp (c : FunId) (ys : Array Arg) : M Unit := do
-  if c == `hugeFuel then
-    throw "the auxiliary constant `hugeFuel` cannot be used in code, it is used internally for compiling `partial` definitions"
   let decl ← getDecl c
   unless ys.size == decl.params.size do
     throw s!"incorrect number of arguments to '{c}', {ys.size} provided, {decl.params.size} expected"