title: How to let COQ write complete proof log?
body: <p>I want COQ to log all its subgoals while executing a proof.
  The -verbose option of COQC did not give the proper result.</p>
  
  <p>Second, is there an option that let COQ log all elementary tactics used by the auto, intuition, etc. tactics?</p>