Fast path in weak head reduction of applied atoms.

Instead of calling the whole reduction machirery, we check before reducing that
a term is an applied atom, i.e. inductive, constructor, evar or meta. In that
case, the abstract machine acts as the identity but needs to destruct and
reconstruct the whole term, which can be very costly.

This fixes part of bug #5421: vm_compute is very slow at doing nothing, where
recomputation of the type of a big inductive was incredibly expensive.

0 files changed, 0 insertions, 0 deletions