Add undohist
Hook onto proof-mode instead of coq-mode