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.
Forgotten hints.ml{,i} files in 38b34dfffcc.
Applying Virgile Prevosto's patch for better error report in coqdep (#3029).