v8.4: Little fix for Nsatz: hypotheses not directly relevant to the nsatz
problem are cleared (in case they denote applicative terms with at
least 6 arguments). However some of them are used for type class
instance inference (e.g. hypotheses of type Integral_domain).

This commits prevents clearing these hypotheses.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16484 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Protection against "Bad recursive type" in w_unify0 (bug #3036).

Morally, unification wants to unify "fun x:Meta => Meta"
with "fun x:nat => match x with ... end". Retyping is asked to
type "match x with ... end" in the context "x:Meta" where the
type of x has de facto been lost. Retyping fails.

I don't see an easy remedy since w_unify0 builds the unifier
lazily, and I'm not sure it is worth to propagate the unifier to
retyping so that it knows it. After all, the call to retyping in
w_unify0 is not so critical.

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