v8.4: A slightly more efficient test of well-typedness of restriction of
evars (though this might be slighty more costly).

This incidentally solves Appel's part of bug #2830 even though a
conceptual problem around the interaction of unification with the
proof engine has to be solved. Indeed, what to do when unification,
called as part of a tactic, solves or refines the current goal by side
effect. Somehow, unifyTerms or tclEVARS should take this possibility
into consideration, either by forbidding the refinement of the current
goal by side effect, or by acknowledging this refinement by producing
new subgoals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/branches/v8.4@16233 85f007b7-540e-0410-9357-904b9bb8a0f7
v8.4: Added missing documentation of Set Printing Existential Instances.

Also started a preliminary documentation about evars (where to have it
in the doc is somehow open).

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