aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
AgeCommit message (Expand)Author
2018-08-29Merge PR #8274: Restore previous printing filtering; always reprint the conte...Emilio Jesus Gallego Arias
2018-08-28Fix typo in comment, sollicited --> solicited.Nick Lewycky
2018-08-24Bug fix: restore previous printing behavior that was unintentionally changed ...Jim Fehrle
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-05-21[stm] Make toplevels standalone executables.Emilio Jesus Gallego Arias
2018-05-08[toplevel] Don't ignore output filename provided by user in -oEmilio Jesus Gallego Arias
2018-05-02Making explicit that errors happen in one of five executation phases.Hugo Herbelin
2018-05-02Reporting when an error occurs at initialization time.Hugo Herbelin
2018-05-01Merge PR #7305: [toplevel] improve indentationEmilio Jesus Gallego Arias
2018-04-23improve indentationEnrico Tassi
2018-04-19[toplevel] let toploop_init change Coq optionsEnrico Tassi
2018-04-07[toplevel] Fix path initialization before vio processing (closes #7044)Emilio Jesus Gallego Arias
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-07[toplevel] Respect COQ_COLORS environment variableThomas Hebb
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-02-28[toplevel] Update state when `Drop` exception is thrown [#6872]Emilio Jesus Gallego Arias
2018-02-28[toplevel] Move beautify to its own pass.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[toplevel] Small refactoring of fatal_error functions.Emilio Jesus Gallego Arias
2018-02-09[toplevel] Refactor command line argument handling.Emilio Jesus Gallego Arias
2018-02-07[toplevel] Disable error resiliency in `-quick` mode.Emilio Jesus Gallego Arias
2018-02-05[stm] [toplevel] Make loadpath a parameter of the document.Emilio Jesus Gallego Arias
2018-02-05[toplevel] Refine start of interactive mode conditions.Emilio Jesus Gallego Arias
2018-01-31[stm] Move options to a per-document record.Emilio Jesus Gallego Arias
2018-01-29[toplevel] Refactor load path handling.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-14Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Maxime Dénès
2017-12-14Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Maxime Dénès
2017-12-11[flags] [stm] Reorganize flags.Emilio Jesus Gallego Arias
2017-12-10[build] Remove coqmktop in favor of ocamlfind.Emilio Jesus Gallego Arias
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-02[kernel] Patch allowing to disable VM reduction.Emilio Jesus Gallego Arias
2017-11-27Merge PR #6207: [stm] Allow delayed constant in interactive mode.Maxime Dénès
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-21[stm] Allow delayed constant in interactive mode.Emilio Jesus Gallego Arias
2017-10-28[toplevel] Export the last document seen after `Drop`.Emilio Jesus Gallego Arias
2017-10-20Merge PR #1147: Remove GeoProof support.Maxime Dénès
2017-10-11Remove GeoProof support.Maxime Dénès
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
2017-10-06[coqtop] Don't reset coqinit internal variables after initialization.Emilio Jesus Gallego Arias
2017-10-05Merge PR #1069: Improve support for -w optionsMaxime Dénès
2017-09-22Merge PR #1070: Remove remaining occurrences of -just-parsing.Maxime Dénès
2017-09-21Remove remaining occurrences of -just-parsing.Guillaume Melquiond
2017-09-21Handle multiple -w options on command line (bug #5736).Guillaume Melquiond
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-08-29Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 12:23:01 +0000