Io.Log
val trace : string -> ?extra:string -> string -> unit
Debug trace
val feedback : Loc.t Coq.Message.t list -> unit
For unexpected feedback, remove eventually or just assert false?