aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
AgeCommit message (Expand)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-09-01Unify the shelvesMaxime Dénès
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
2020-04-15[proof] Move functions related to `Proof.t` to `Proof`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-04[boot] Don't initialize coqlib when `-boot` is passed.Emilio Jesus Gallego Arias
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-13Merge PR #11521: Remove Goptions.opt_name fieldPierre-Marie Pédrot
2020-02-12[toplevel] Make toplevel loop tail-recursive againEmilio Jesus Gallego Arias
2020-02-12[toplevel] Refactor control loopEmilio Jesus Gallego Arias
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-01-30coqtop: stop on Sys_blocked_ioGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-08A classification of command line options.Hugo Herbelin
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-11-24Merge PR #8950: [topfmt] Add phase attribute for toplevel printing.Hugo Herbelin
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
2018-11-09[topfmt] Add phase attribute for toplevel printing.Emilio Jesus Gallego Arias
2018-11-04Remove the deprecated Token module and port the corresponding code.Pierre-Marie Pédrot
2018-08-24Bug fix: restore previous printing behavior that was unintentionally changed ...Jim Fehrle
2018-07-31Code to handle "Back" command for diffs.Jim Fehrle
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:36 +0000