aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqloop.ml
AgeCommit message (Expand)Author
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
2018-04-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
2018-04-04Merge PR #7144: [toplevel] Protect goal printing better wrt Break [helps with...Enrico Tassi
2018-04-01[toplevel] Protect goal printing better wrt Break [fixes #7142]Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-05[toplevel] Modify printing goal strategy.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-15[toplevel] Make toplevel state into a record.Emilio Jesus Gallego Arias
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01[emacs] [toplevel] Make emacs flag local to the toplevel.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 18:04:42 +0000