aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* 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
| * | [make] remove unneeded generated file "tolink.ml"Gravatar Emilio Jesus Gallego Arias2017-12-10
| * | [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
|\
* | [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* | [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
|\
* | [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
| * 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 #1106: Fix beautifierGravatar Maxime Dénès2017-10-05
|\ \
| * | Remove catch-all try with in the beautifier.Gravatar Théo Zimmermann2017-09-27
| * | Beautifier gets its own formatter: fixes BZ#5704.Gravatar Théo Zimmermann2017-09-27
* | | [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
|/ /
* | Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\ \
* \ \ 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
|/ /
| * Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* 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
* | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |/ |/|
| * Also a less intrusive Profile.init_profile.Gravatar Hugo Herbelin2017-07-20
|/
* Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* "There are pending proofs" error message now lists the name of the proofs.Gravatar Théo Zimmermann2017-06-16
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#758: [toplevel] Print error header on fatal batch error.Gravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \
| | | * Add support for Coq 8.6.Gravatar Guillaume Melquiond2017-06-14
| | | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | * Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 08:56:56 +0000