Fixed bad newlines in output for std output and emacs.

I added a emacs_logger.
Still need to cleanup std_logger.
Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for grammar in campl4
Proof using: New vernacular to name sets of section variables
Cleaning up universe list implementation in Univ.

We use private types to ensure apriori hashconsing, and get rid of the
use of recursive modules. The hash of the universe list is also inlined
into each node instead of relying on a supplementary indirection.
Backporting the change in lists of universes to the checker.
Fixing checker representation of universe lists.
Lists: a few results on Exists and Forall and a bit of code cleanup.
Lists: enhanced version of Seb's last commit on Exists/Forall
Implement the nodup function on lists and prove associated results.
Adds two lemmas about hderror to the List standard library.