Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.

Some functions moved to the new proof engine.
Adding a printer for hints.