aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-04-02Remove -compat 8.7Jason Gross
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-01Move test_mode from Flags to Vernacentries (use point)Gaëtan Gilbert
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-26Initialize styles so textual markers are used when color is not enabledJim Fehrle
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-20[paths] Try to be more portable on Win32Emilio Jesus Gallego Arias
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-02-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
2019-02-01[toplevel] Split interactive toplevel and compiler binaries.Emilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2019-01-27Merge PR #9263: [STM] explicit handling of parsing statesEmilio Jesus Gallego Arias
2019-01-24Update -compat to support -compat 8.10Jason Gross
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2019-01-08Fix #3934: coqc -time -quick gives unreadable outputMaxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:55:06 +0000