diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 8018df6569..38cf690198 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -35,9 +35,6 @@ option(STATIC             "STATIC"             OFF)
 option(SPLIT_STACK        "SPLIT_STACK"        OFF)
 # When OFF we disable LLVM support
 option(LLVM               "LLVM"               OFF)
-option(COMPRESSED_OBJECT_HEADER "Use compressed object headers in 64-bit machines, this option is ignored in 32-bit machines, and assumes the 64-bit OS can only address 2^48 bytes" ON)
-option(SMALL_RC "Use only 32-bits for RC, this option is only relevant when COMPRESSED_OBJECT_HEARDER is ON" ON)
-option(CHECK_RC_OVERFLOW "Check for RC overflows when SMALL_RC is ON" OFF)
 
 # Include MSYS2 required DLLs and binaries in the binary distribution package
 option(INCLUDE_MSYS2_DLLS "INCLUDE_MSYS2_DLLS" OFF)
@@ -91,26 +88,6 @@ else()
   set(NumBits 32)
 endif()
 
-if ("${COMPRESSED_OBJECT_HEADER}" MATCHES "ON")
-  if (NumBits EQUAL "64")
-    if ("${SMALL_RC}" MATCHES "ON")
-        set(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC "#define LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC")
-        message(STATUS "Using compressed object headers and only 32-bits for reference counter, this feature assume the OS only uses memory addresses < 2^48")
-        if ("${CHECK_RC_OVERFLOW}" MATCHES "ON")
-           set(LEAN_CHECK_RC_OVERFLOW "#define LEAN_CHECK_RC_OVERFLOW")
-           message(STATUS "RC overflow checks are enabled")
-        endif()
-    else()
-        set(LEAN_COMPRESSED_OBJECT_HEADER "#define LEAN_COMPRESSED_OBJECT_HEADER")
-        message(STATUS "Using compressed object headers, this feature assume the OS only uses memory addresses < 2^48")
-    endif()
-  else()
-    message(STATUS "Compressed object headers cannot be used in 32-bit machines")
-  endif()
-else()
-    message(STATUS "Using big object headers")
-endif()
-
 if ("${RUNTIME_STATS}" MATCHES "ON")
   set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_RUNTIME_STATS")
   set(LEANC_EXTRA_FLAGS "${LEANC_EXTRA_FLAGS} -D LEAN_RUNTIME_STATS")
diff --git a/src/config.h.in b/src/config.h.in
index f109cc37a6..193bb56aa7 100644
--- a/src/config.h.in
+++ b/src/config.h.in
@@ -9,7 +9,4 @@ Author: Leonardo de Moura
 
 @LEAN_SMALL_ALLOCATOR@
 @LEAN_LAZY_RC@
-@LEAN_COMPRESSED_OBJECT_HEADER@
-@LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC@
-@LEAN_CHECK_RC_OVERFLOW@
 @LEAN_IS_STAGE0@
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 368c42a9fd..4fa9bcc730 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -82,16 +82,26 @@ static inline bool lean_is_big_object_tag(uint8_t tag) {
 
 LEAN_CASSERT(sizeof(size_t) == sizeof(void*));
 
-#if defined(LEAN_COMPRESSED_OBJECT_HEADER) || defined(LEAN_COMPRESSED_OBJECT_HEADER_SMALL_RC)
-/* Compressed headers are only supported in 64-bit machines */
-LEAN_CASSERT(sizeof(void*) == 8);
-#endif
+/*
+Lean object header.
 
-/* Lean object header */
+The reference counter `m_rc` field also encodes whether the object is single threaded (> 0), multi threaded (< 0), or
+reference counting is not needed (== 0). We don't use reference counting for objects stored in compact regions, or
+marked as persistent.
+
+For "small" objects stored in compact regions, the field `m_cs_sz` contains the object size. For "small" objects not
+stored in compact regions, we use the page information to retrieve its size.
+
+During deallocation and 64-bit machines, the fields `m_rc` and `m_cs_sz` store the next object in the deletion TODO list.
+These two fields together have 48-bits, and this is enough for modern computers.
+In 32-bit machines, the field `m_rc` is sufficient.
+
+The field `m_other` is used to store the number of fields in a constructor object and the element size in a scalar array.
+*/
 typedef struct {
-    int      m_rc;        /* > 0 - single thread object, < 0 - multi threaded object, == 0 - persistent object. */
-    unsigned m_cs_sz:16;  /* for small objects stored in compact regions, this field contains the object size. It is 0, otherwise */
-    unsigned m_other:8;   /* number of fields for constructors, element size for scalar arrays */
+    int      m_rc;
+    unsigned m_cs_sz:16;
+    unsigned m_other:8;
     unsigned m_tag:8;
 } lean_object;