Type-checking time at QED should not be slower than evaluating the tactics building the proof. A typical cause of being slower (and even exponentially slower) is that the type-checker does not preserve the history of reduction steps used in the proof (unfold, simpl, …) and try to recheck from scratch why two terms are convertible (see e.g. this typical example of long Qed : "Qed." takes a long time). In principle, it is certainly possible to do something but I don’t know precisely how far some developers are already looking on their free time at this issue or not.