aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-12-10For diffs, return exactly the characters that make up STRING and FIELD tokensJim Fehrle
2018-12-10Fix #9091: don't show deleted compacted hypotheses twice in diffJim Fehrle
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
2018-12-10[coq] Adapt to coq/coq#9172Emilio Jesus Gallego Arias
2018-12-10List members of the code of conduct enforcement team.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-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
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 pull request coq/ltac2#90 from ejgallego/testsPierre-Marie Pédrot
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 pull request #20 from ejgallego/vernac+remove_empty_hooksEmilio Jesús Gallego Arias
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-05Add test for #8951.Gaëtan Gilbert
2018-12-05Fix mod_subst wrt universe polymorphismGaë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