aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
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[make] remove unneeded generated file "tolink.ml"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[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
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-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
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-10-05Merge PR #1106: Fix beautifierMaxime Dénès
2017-09-27Remove catch-all try with in the beautifier.Théo Zimmermann
2017-09-27Beautifier gets its own formatter: fixes BZ#5704.Théo Zimmermann
2017-09-27[stm] Warn about costly Undo operations in batch mode [BZ#5677]Emilio Jesus Gallego Arias
2017-09-22Merge PR #1055: Remove STM vernacularsMaxime 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-09-19Remove STM vernaculars.Maxime Dénès
2017-09-14Using an algebraic type for distinguishing toplevel input from location in file.Hugo Herbelin
2017-08-29Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Maxime Dénès
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-08-01Merge PR #917: Moving --print-version to -print-version for consistency.Maxime Dénès
2017-07-31[general] Remove spurious dependency of highparsing on toplevel.Emilio Jesus Gallego Arias
2017-07-27[toplevel] Remove long ago deprecated and NOOP options.Emilio Jesus Gallego Arias
2017-07-26Merge PR #902: Only perform profile initialization and printing when the flag...Maxime Dénès
2017-07-25Adding -print-version in addition to -print-version for consistency.Hugo Herbelin
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-20Also a less intrusive Profile.init_profile.Hugo Herbelin
2017-07-08Adding support for bindings tags to explicit prefix/suffix rather than colors.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16"There are pending proofs" error message now lists the name of the proofs.Théo Zimmermann
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#758: [toplevel] Print error header on fatal batch error.Maxime Dénès
2017-06-14Merge PR#763: [proof] Deprecate redundant wrappers.Maxime Dénès
2017-06-14Add support for Coq 8.6.Guillaume Melquiond
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond