Un-deprecate to_integer(constant_exprt)

tautschnig · tautschnig · commit 92159fa956b5 · 2018-06-07T13:27:22.000Z
The recommended substitute uses this function, removing it is currently
impossible.
diff --git a/src/util/arith_tools.h b/src/util/arith_tools.h
@@ -27,8 +27,6 @@ DEPRECATED("Use the constant_exprt version instead")
 bool to_integer(const exprt &expr, mp_integer &int_value);
 
 // returns 'true' on error
-/// \deprecated: use numeric_cast<mp_integer> instead
-DEPRECATED("Use numeric_cast<mp_integer> instead")
 bool to_integer(const constant_exprt &expr, mp_integer &int_value);
 
 // returns 'true' on error
