aboutsummaryrefslogtreecommitdiff
path: root/library/goptions.ml
AgeCommit message (Expand)Author
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-20Improve undeclared key messages.Théo Zimmermann
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-03Improve error messages for Set and Unset commands.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-29Make sure that all query commands return a notice (not an info) feedbackMaxime Dénès
2019-06-25Merge PR #10284: Expose set interface to option tablesPierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-03Expose set interface to option tablesGaëtan Gilbert
2019-04-30Remove Global.env from goptions by passing from vernacentriesGaëtan Gilbert
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-23Goptions.declare_* functions return unit instead of a write_functionGaëtan Gilbert
2018-11-05[Goptions] More detailed error messagesVincent Laporte
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-07-26Add information to option type errorsTej Chajed
2018-06-18Remove reference name type.Maxime Dénès
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-09Export the various option localities in the API.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2016-12-19Use Pp.quote in string options.Maxime Dénès
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-02Fix various shortcomings of the warnings infrastructure.Maxime Dénès
2016-11-02Put string between quotes when printing an option value.Maxime Dénès
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-04Changing the separator for appended string options to comma.Maxime Dénès
2016-10-01Allow appending to string options.Guillaume Melquiond
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-06A proposal to unify the messages given by Test and Print Options (#5062).Hugo Herbelin
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-10-08Goptions: new value type: optional stringEnrico Tassi
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-02-17Deprecated options issue a warning.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:41:28 +0000