aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Merge PR #8727: [options] New helper for creation of boolean options plus ref...Pierre-Marie Pédrot
2018-11-28Merge PR #8826: [toplevel] Allow to specify default options.Pierre-Marie Pédrot
2018-11-28[options] New helper for creation of boolean options plus reference.Emilio Jesus Gallego Arias
2018-11-27Make `-async-proofs on` effective with `coqc`Maxime Dénès
2018-11-27Remove -async-proofs-full flagMaxime Dénès
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-24[toplevel] Allow to specify default options.Emilio Jesus Gallego Arias
2018-11-24[toplevel] Move compilation-related functions to their own module.Emilio Jesus Gallego Arias
2018-11-24[toplevel] Move command line path processing to CoqargsEmilio 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-16Do not Export the init modulesGaëtan Gilbert
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-09[topfmt] Add phase attribute for toplevel printing.Emilio Jesus Gallego Arias
2018-11-05Merge PR #8899: Remove the deprecated Token module and port the corresponding...Emilio Jesus Gallego Arias
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-11-04Remove the deprecated Token module and port the corresponding code.Pierre-Marie Pédrot
2018-10-29[gramlib] Wrap `Gramlib`.Emilio Jesus Gallego Arias
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
2018-10-02Update the -compat flagsJason Gross
2018-10-01[lib] [flags] Move coqlib handling out of `Flags`Emilio Jesus Gallego Arias
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-09-02Make -compat 8.8 import Coq.Compat.Coq88Jason Gross
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-08-17Remove dead argument allow_old.Théo Zimmermann
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-06-29Port g_toplevel to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-19[coqtop] Give priority to stdlib load path over current directoryMaxime Dénès
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-21[ide] Remove special option `-ideslave`Emilio Jesus Gallego Arias
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-11[warnings] Remove `set_current_loc` hack.Emilio Jesus Gallego Arias
2018-04-07[toplevel] Fix path initialization before vio processing (closes #7044)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