aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-02-22Merge PR #9314: Enrich implicits for instancesGaëtan Gilbert
2019-02-22Merge PR #9539: [coqdoc] Add the From keywordGaëtan Gilbert
2019-02-22Implement hmap.updateGaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-22[lib] Add `Map.update` from OCaml 4.06Emilio Jesus Gallego Arias
2019-02-22Merge PR #9614: Fix #9613 use -coqlib when invoking coqchkEmilio Jesus Gallego Arias
2019-02-21Merge PR #9588: [azure] [ci] Build on Windows using Dune.Gaëtan Gilbert
2019-02-21Stdlib HTML documentation: fix a few absolute URLsVincent Laporte
2019-02-21Merge PR #9577: [Namegen] Use Global.exists_objlabel in `next_global_ident_away`Pierre-Marie Pédrot
2019-02-21Merge PR #9618: [dev/tools/create_overlays] remove trailing whitespaceEmilio Jesus Gallego Arias
2019-02-21remove meta trailing whitespaceEnrico Tassi
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaëtan Gilbert
2019-02-21Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shel...Emilio Jesus Gallego Arias
2019-02-20Merge PR #9529: Change Primitive message: "is registered" -> "is declared".Vincent Laporte
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
2019-02-20Merge PR #9457: Correct W-Ind in Cic description of the reference manual.Théo Zimmermann
2019-02-20[paths] Try to be more portable on Win32Emilio Jesus Gallego Arias
2019-02-20[azure] [ci] Build on Windows using Dune.Emilio Jesus Gallego Arias
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-19Merge PR #9501: Sphinx: fail when a command fails + other stuffClément Pit-Claudel
2019-02-19Merge PR #9297: Two fixes in printing notations with patternsEmilio Jesus Gallego Arias
2019-02-19Merge PR #9604: Gramlib: Fixes #9358 (ensuring that requested locations are e...Emilio Jesus Gallego Arias
2019-02-19Merge PR #9603: Make inductive cumulativity flag local to vernacentriesEmilio Jesus Gallego Arias
2019-02-19Gramlib: Fixes #9358 (ensuring that the loc function has something to compute).Hugo Herbelin
2019-02-19Notations: Fixing a printing bug with patterns.Hugo Herbelin
2019-02-19Notations: Enforce strong evaluation of cases_pattern_of_glob_constr.Hugo Herbelin
2019-02-19[sphinx] Refactor handling of options for coqtop directive.Théo Zimmermann
2019-02-19Make inductive cumulativity flag local to vernacentriesGaëtan Gilbert
2019-02-19Make the conclusion of local contexts W-Ind empty.Tanaka Akira
2019-02-18Merge PR #9306: Remove Printing Primitive Projection CompatibilityMaxime Dénès
2019-02-18Using options abort and restart of coqtop directive in the manual.Théo Zimmermann
2019-02-18[sphinx] Add abort and restart options to directive coqtop.Théo Zimmermann
2019-02-18coqdomain.py fix typo in commentGaëtan Gilbert
2019-02-18Sphinx: nicer error reportingGaëtan Gilbert
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-18Fix doc for Refine Instance ModeGaëtan Gilbert
2019-02-18Sphinx: remove [coqtop:: undo]Gaëtan Gilbert
2019-02-18Fix last nested lemma failure.Théo Zimmermann
2019-02-18Fix failing coqtops in type-classes.rstGaëtan Gilbert
2019-02-18Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linterThéo Zimmermann
2019-02-18Merge PR #9589: Deprecate duplicated explicitation_eqEmilio Jesus Gallego Arias
2019-02-18Merge PR #9600: CI: fix trunk jobs switch pickingEmilio Jesus Gallego Arias
2019-02-18Merge PR #9597: [ci] Resolve commit corresponding to branch when downloading ...Emilio Jesus Gallego Arias
2019-02-18Merge PR #9142: Disable Ltac backtracesHugo Herbelin
2019-02-18Merge PR #9592: Fix per-commit linting with bot mergesEmilio Jesus Gallego Arias
2019-02-18Merge PR #9599: Remove undefined install_printer ppcumulativity_infoEmilio Jesus Gallego Arias
2019-02-18[dev] Add include versions for Dune builds.Emilio Jesus Gallego Arias
2019-02-18CI: fix trunk jobs switch pickingGaëtan Gilbert
2019-02-18Remove undefined install_printer ppcumulativity_infoGaëtan Gilbert
2019-02-18[ci] Resolve commit corresponding to branch when downloading tarball.Théo Zimmermann