From babdde90686880fb4358204fa166f02e0630756b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Mar 2021 07:54:43 -0800
Subject: [PATCH] chore: activate `decide` and `nativeDecide`

---
 src/Lean/Elab/Tactic/ElabTerm.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 8f48b6d6eb..99ce562743 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -155,8 +155,6 @@ private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
     throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
   return expectedType
 
-#exit -- TODO remove after update stage0
-
 @[builtinTactic Lean.Parser.Tactic.decide] def evalDecide : Tactic := fun stx =>
   closeMainUsing fun expectedType => do
     let expectedType ← preprocessPropToDecide expectedType