aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* Making explicit that errors happen in one of five executation phases.Gravatar Hugo Herbelin2018-05-02
* Reporting when an error occurs at initialization time.Gravatar Hugo Herbelin2018-05-02
* Merge PR #7305: [toplevel] improve indentationGravatar Emilio Jesus Gallego Arias2018-05-01
|\
| * improve indentationGravatar Enrico Tassi2018-04-23
* | [toplevel] let toploop_init change Coq optionsGravatar Enrico Tassi2018-04-19
|/
* [toplevel] Fix path initialization before vio processing (closes #7044)Gravatar Emilio Jesus Gallego Arias2018-04-07
* [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
* [toplevel] Respect COQ_COLORS environment variableGravatar Thomas Hebb2018-03-07
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \
* | | [toplevel] Update state when `Drop` exception is thrown [#6872]Gravatar Emilio Jesus Gallego Arias2018-02-28
| * | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
|/ /
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [toplevel] Make toplevel state into a record.Gravatar Emilio Jesus Gallego Arias2018-02-15
* [toplevel] Small refactoring of fatal_error functions.Gravatar Emilio Jesus Gallego Arias2018-02-09
* [toplevel] Refactor command line argument handling.Gravatar Emilio Jesus Gallego Arias2018-02-09
* [toplevel] Disable error resiliency in `-quick` mode.Gravatar Emilio Jesus Gallego Arias2018-02-07
* [stm] [toplevel] Make loadpath a parameter of the document.Gravatar Emilio Jesus Gallego Arias2018-02-05
* [toplevel] Refine start of interactive mode conditions.Gravatar Emilio Jesus Gallego Arias2018-02-05
* [stm] Move options to a per-document record.Gravatar Emilio Jesus Gallego Arias2018-01-31
* [toplevel] Refactor load path handling.Gravatar Emilio Jesus Gallego Arias2018-01-29
* [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Gravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \
* | | [flags] [stm] Reorganize flags.Gravatar Emilio Jesus Gallego Arias2017-12-11
| * | [build] Remove coqmktop in favor of ocamlfind.Gravatar Emilio Jesus Gallego Arias2017-12-10
| * | [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
|/ /
| * [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
|/
* Merge PR #6207: [stm] Allow delayed constant in interactive mode.Gravatar Maxime Dénès2017-11-27
|\
* | [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| * [stm] Allow delayed constant in interactive mode.Gravatar Emilio Jesus Gallego Arias2017-11-21
|/
* [toplevel] Export the last document seen after `Drop`.Gravatar Emilio Jesus Gallego Arias2017-10-28
* Merge PR #1147: Remove GeoProof support.Gravatar Maxime Dénès2017-10-20
|\
| * Remove GeoProof support.Gravatar Maxime Dénès2017-10-11
* | [stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Gravatar Emilio Jesus Gallego Arias2017-10-11
|/
* [stm] Switch to a functional APIGravatar Emilio Jesus Gallego Arias2017-10-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* [coqtop] Don't reset coqinit internal variables after initialization.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Merge PR #1069: Improve support for -w optionsGravatar Maxime Dénès2017-10-05
|\
* \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \
| * | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
| | * Handle multiple -w options on command line (bug #5736).Gravatar Guillaume Melquiond2017-09-21
| |/
* / [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/
* Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Gravatar Maxime Dénès2017-08-29
|\
* | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* | Merge PR #917: Moving --print-version to -print-version for consistency.Gravatar Maxime Dénès2017-08-01
|\ \
| | * [general] Remove spurious dependency of highparsing on toplevel.Gravatar Emilio Jesus Gallego Arias2017-07-31
* | | [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ |/|
* | Merge PR #902: Only perform profile initialization and printing when the flag...Gravatar Maxime Dénès2017-07-26
|\ \
| | * Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25