The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

You might try replacing "eval compute" with "eval hnf" so it only does
the computation needed to determine which constructor the result is,
and not computation of the internal details of proofs.  If that still
doesn't make things efficient enough, you might try writing an
intermediate function MyRel_dec_int : forall a b, Acc lt (weight_fn a
b) -> {MyRel a b} + {~MyRel a b} which is a fixed point on the Acc
predicate.  Then, use the trick of expanding the Acc proof 2^N times
and feeding that into MyRel_dec_int instead of your original Acc
proof, to define MyRel_dec.  (Sorry I don't recall the details of how
the expansion of Acc is written off the top of my head, but it's been
posted several times before in the mailing list.)
-- 
Daniel Schepler