aboutsummaryrefslogtreecommitdiff
path: root/lib/feedback.mli
AgeCommit message (Expand)Author
2019-08-29Remove wrong advice to base feedback level choice on encoding issuesMaxime Dénès
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 2JPR
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-12[stm] Remove edit_id.Emilio Jesus Gallego Arias
2017-03-21[pp] Debug feeder is not needed anymore.Emilio Jesus Gallego Arias
2017-03-21[pp] Make feedback the only logging mechanism.Emilio Jesus Gallego Arias
2017-03-21[feedback] Allow to remove feedback listeners.Emilio Jesus Gallego Arias
2016-11-10Remove unused feedback_content: GoalsCJ Bell
2016-09-30[pp] Remove duplicate color logger.Emilio Jesus Gallego Arias
2016-09-13feedback: provide a feeder that prints debug messagesEnrico Tassi
2016-09-05feedback: support multiple feedback listenersEnrico Tassi
2016-06-25[feedback] Remove `ErrorMsg` in favor of `Message Error`.Emilio Jesus Gallego Arias
2016-06-25[feedback] Allow messages to carry a location.Emilio Jesus Gallego Arias
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove unused tag on `Debug` level.Emilio Jesus Gallego Arias
2016-06-02Encapsulate xml serialization in xmlprotocol.mliEmilio Jesus Gallego Arias
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-10-31Feedback message: hold extra info to help routingEnrico Tassi
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
2014-10-01STM: report the (structured) goals as XMLCarst Tankink
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-08-04STM: encapsulate Pp.message in Feedback.feedbackCarst Tankink
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-06-25all coqide specific files moved into ide/Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:59:28 +0000