Mod_subst: an extra assert

It seems that the Equiv delta_hint in a resolver have a particular shape:
a kn can apparently only be shifted to another kn with same label
this way. We validate this fact via an assert, since this isn't
obvious (due to recursive calls in Mod_subst and Modops), and since
this implies the important fact that user and canonical parts
of kernel pairs have necessarily the same label (and section dirpath).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16219 85f007b7-540e-0410-9357-904b9bb8a0f7
module_path --> ModPath.t, kernel_name --> KerName.t

For the moment, the compatibility names about these new modules
are still used in the rest of Coq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16220 85f007b7-540e-0410-9357-904b9bb8a0f7
Dir_path --> DirPath

 Ok, this is merely a matter of taste, but up to now the usage
 in Coq is rather to use capital letters instead of _ in the
 names of inner modules.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
avoid (Int.equal (cmp ...) 0) when a boolean equality exists

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16222 85f007b7-540e-0410-9357-904b9bb8a0f7