Apia doesn't support Agda "dead code" new feature

[asr]

From @asr on September 30, 2015 15:46

Agda is using a dead code analysis for reducing the interfaces file. Apia currently doesn't support this "feature".

At the moment, we removed the dead code analysis from eagda (see https://github.com/asr/eagda/commit/3dbd2a6378073067db25d87d40dccbf7490cb1c7).

[asr]

I revert the eagda commit https://github.com/asr/eagda/commit/3dbd2a6378073067db25d87d40dccbf7490cb1c7 in https://github.com/asr/eagda/commit/7f8ce15eb38ccfe3a5bff0eea929c0c8af0f06ad.

[asr]

module Bug where

postulate
  D   : Set
  _≡_ : D → D → Set
  d e : D

foo : ∀ x → x ≡ x
foo x = bar
  where
  postulate
    d≡e : d ≡ e

  postulate
    bar : x ≡ x
  {-# ATP prove bar d≡e #-}

-- $ apia Bug.agda
-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/Apia/Utils/AgdaAPI/Interface.hs:307

-- The error occurs because the dead code analysis removes `d≡e` from
-- the interface file.

[asr]

I revert the revert of https://github.com/asr/eagda/commit/3dbd2a6378073067db25d87d40dccbf7490cb1c7 in https://github.com/asr/eagda/commit/75f338a21fb1d9f1c0cece25dba5549f656cf6f2.