aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-21Merge PR #11075: load .vo when .vos is missing + misc vos changesEmilio Jesus Gallego Arias
2019-11-20From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...charguer
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall th...charguer
2019-11-01Implementing support for vos/vok files.charguer
2019-10-31[prettyp] remove `mod_ops` and `indirect_accessor` parametersGaëtan Gilbert
2019-10-29Show diffs in "Show Proof."Jim Fehrle
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
2019-10-11Merge PR #10489: Fix output for "Printing Dependent Evars Line"Hugo Herbelin
2019-10-11Merge PR #10697: [vernac] Split vernacular translation and interpretation.Gaëtan Gilbert
2019-10-07Call to update-compat.py.Pierre-Marie Pédrot
2019-10-07[vernac] Split vernacular translation and interpretation.Emilio Jesus Gallego Arias
2019-10-04Allow SProp default onGaëtan Gilbert
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-09-09Merge PR #10605: [toplevel] Make all argument lists to be in user-declared or...Hugo Herbelin
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to `EM...Emilio Jesus Gallego Arias
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-07-31[toplevel] Make all argument lists to be in user-declared order.Emilio Jesus Gallego Arias
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
2019-07-08Usage: bypassing a useless detour via a reference.Hugo Herbelin
2019-07-08An even more uniform treatment of the -help option across executables.Hugo Herbelin
2019-07-08Removing -filterops "hack" from coqtop.Hugo Herbelin
2019-07-08Some common points between coqc and other coq binaries.Hugo Herbelin
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
2019-07-08An attempt to reorganize further coqtop initialization into semantic units.Hugo Herbelin
2019-07-08Adding methods help and parse_extra to custom toplevels data.Hugo Herbelin
2019-07-08Function print_memory_stat: getting rid of a mutable.Hugo Herbelin
2019-07-08A classification of command line options.Hugo Herbelin
2019-07-08Toplevel: structuring init_toplevel.Hugo Herbelin
2019-07-08Toplevel: structuring source code.Hugo Herbelin
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:14:21 +0000