A few optimizations around kernel_names...

 For instance, let's avoid computing twice subst_mp when possible.
 Interest: small speed-up, but also improved sharing of results,
 hence slightly smaller vo.

 Inspired by changes already done in trunk, but I won't backport
 to 8.4 the more radical changes done recently (pairs of kernel_names
 not coded as pairs anymore when possible).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16319 85f007b7-540e-0410-9357-904b9bb8a0f7