aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-11Merge PR #9197: Fixing imports in debug printers: gramlib depends on Loc whic...Emilio Jesus Gallego Arias
2018-12-11Merge PR #8655: Test suite: use coqc and then coqchkEnrico Tassi
2018-12-11Merge PR #9155: Fix race condition triggered by fresh universe generationEnrico Tassi
2018-12-11Fixing imports in debug printers: gramlib depends on Loc which is in lib.cma.Hugo Herbelin
2018-12-11Merge PR #9151: [dune] Teach coq_dune about `.glob` and `.aux` files.Théo Zimmermann
2018-12-10[test-suite] Fail when the checker failsVincent Laporte
2018-12-10[test-suite] Run `coqchk` on most test casesVincent Laporte
2018-12-10[dune] Teach coq_dune about `.glob` and `.aux` files.Emilio Jesus Gallego Arias
2018-12-10Merge PR #9145: Do so that an error message follows the "Error:" header on th...Emilio Jesus Gallego Arias
2018-12-10Merge PR #9077: Rename generated directory gramlib__pack -> gramlib/.packEmilio Jesus Gallego Arias
2018-12-10Merge PR #9177: add relation-algebra to CI test suiteGaëtan Gilbert
2018-12-10Merge PR #9106: [dune] Install coq libraries in `%{lib_root}/coq` instead of ...Vincent Laporte
2018-12-10Merge PR #7221: The usual order of strings.Hugo Herbelin
2018-12-09fix copy-paste error in CI_ARCHIVEURLChristian Doczkal
2018-12-09add relation-algebra to CI test suiteChristian Doczkal
2018-12-08[dune] Install coq libraries in `%{lib_root}/coq` instead of `lib`Emilio Jesus Gallego Arias
2018-12-08Do so that an error message follows the "Error:" header on the same line.Hugo Herbelin
2018-12-07Merge PR #8811: EConstr-aware functions to produce kernel entriesPierre-Marie Pédrot
2018-12-06Merge PR #9140: [ci] Add four color theorem proof to CIGaëtan Gilbert
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06High level functions to produce kernel entries from econstr.Gaëtan Gilbert
2018-12-06Evarutil.finalize: combine minimize, to_constr and restrict.Gaëtan Gilbert
2018-12-06Rename generated directory gramlib__pack -> gramlib/.packGaëtan Gilbert
2018-12-06unignore Makefile.installGaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-06Merge PR #8917: Small cleanup wrt attributes_of_flags and template attributeVincent Laporte
2018-12-06Merge PR #9069: [gramlib] Remove dead codeHugo Herbelin
2018-12-05[ci] Add four color theorem proof to CIEmilio Jesus Gallego Arias
2018-12-05Remove the Like level modifier from gramlib.Pierre-Marie Pédrot
2018-12-05Remove the grammar-entry correspondence dynamic check in camlp5.Pierre-Marie Pédrot
2018-12-05Removing dead fields from Plexing.lexer.Pierre-Marie Pédrot
2018-12-05Remove dead code in camlp5.Pierre-Marie Pédrot
2018-12-05Remove the lexer field from Gramlib.Pierre-Marie Pédrot
2018-12-05Make some camlp5 fields immutable.Pierre-Marie Pédrot
2018-12-05Merge PR #9065: [gramlib] Remove `Ploc.t` in favor of `Loc.t`Pierre-Marie Pédrot
2018-12-05Merge PR #8705: [vernac] [hooks] Refactor towards optional hooks.Pierre-Marie Pédrot
2018-12-05Move template out of Defattributes recordGaëtan Gilbert
2018-12-05attributes_of_flags and its output type now internal in vernacentriesGaëtan Gilbert
2018-12-05Merge PR #8911: Document undocumented flags and optionsThéo Zimmermann
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-12-04Remove undocumented "Proof using Clear Unused" flagJim Fehrle
2018-12-04Merge PR #9134: CI: track dev branch of coq-simple-ioEmilio Jesus Gallego Arias
2018-12-04CI: track dev branch of coq-simple-ioYishuai Li
2018-12-04Merge PR #9127: Remove leftover code that used to handle ml4 files.Emilio Jesus Gallego Arias
2018-12-04Merge PR #8187: Notation printing based on scopes (take 2, including bug fixes)Emilio Jesus Gallego Arias
2018-12-04Remove leftover code that used to handle ml4 files.Pierre-Marie Pédrot
2018-12-04Merge PR #9053: Document code owner team creation.Maxime Dénès
2018-12-04Giving to type_scope a softer role in printing.Hugo Herbelin
2018-12-04Notation.ml: Moving code about binding scopes to coercion classes earlier.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 01:23:33 +0000