Finer fix for bug 3017, mark unresolvability only of goals that are
instances of metas in clenvtac. Makes Math-Classes compile again.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqc: accept -exclude-dir + some others + cleanup (fix #3025)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16430 85f007b7-540e-0410-9357-904b9bb8a0f7
Coqdep: add an -exclude-dir option (wish mentionned in #3025)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16431 85f007b7-540e-0410-9357-904b9bb8a0f7
coqc and coqmktop migrated in tools/, get rid of scripts/ subdir

 No need to place these binaries apart, and anyway they aren't
 (shell) scripts since ages.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16432 85f007b7-540e-0410-9357-904b9bb8a0f7
interface.mli and serialize.ml reworked to avoid copy/paste of types

With this commit the types involved in the protocol between Coq and
Coqide are written once and for all in interface.mli

serialize.ml is monkey code that contains a reified version of these
types and the related machinery needed to marshal values in these types
to/from xml in a modular way.  This file should be automatically
generated from the spec of the protocol in an ideal world.
Phantom types are used to statically check that the reified form
of the types is in sync with the one declared in interface.mli

The benefit of this commit is that changing the protocol is easier:
one changes the types in interface.mli and lets ocamlc spot all the
places that needs to be modified.
This is a necessity if one plays with the protocol very often, like
in my Paral-ITP branch.

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