Add type information in error message when a constructor is not fully
applied in pattern-matching. This provides with a side way for the
user to understand what is happening in the situation
match ... with ... S ... => ... end" where S is supposed to be a
variable but S being taken by Coq as successor in nat.

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