aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-15Merge PR #12323: Fixes #12322: anomaly when printing "fun" binders with impli...Emilio Jesus Gallego Arias
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
2020-05-15Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.Emilio Jesus Gallego Arias
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
2020-05-15Merge PR #12032: [win] Elpi, Coq-Elpi and HBMichael Soegtrop
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ru...Hugo Herbelin
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-05-14Add advisories on OCaml setup to INSTALL.md.Théo Zimmermann
2020-05-14Merge PR #12296: Fixes #12234: wrong environment for Show ProofGaëtan Gilbert
2020-05-14Merge PR #12327: Add a changelog for 8.11.2.Théo Zimmermann
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
2020-05-14Add a changelog for 8.11.2.Pierre-Marie Pédrot
2020-05-14Merge PR #12312: Clarify the documentation for merging PRs with overlaysThéo Zimmermann
2020-05-14Adding changelog.Pierre-Marie Pédrot
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-14Tweak the error message of reference internalization.Pierre-Marie Pédrot
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Generalize the interpretation of syntactic notation as reference to their head.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
2020-05-14Added change log.Hugo Herbelin
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
2020-05-14Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.Gaëtan Gilbert
2020-05-14Merge PR #12320: [ci] [sf] Fix SF build.Gaëtan Gilbert
2020-05-14Merge PR #12214: nit: don't open Persistent_cache in micromegaVincent Laporte
2020-05-14Add changelog for #12323.Hugo Herbelin
2020-05-14Fixes #12322 (anomaly when printing "fun" binders with implicit types).Hugo Herbelin
2020-05-14[ci] [sf] Fix SF build.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12097: Interleave commandline require/set/unset commandsEmilio Jesus Gallego Arias
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
2020-05-14Merge PR #12315: Tests for bugs #9583 (fixed by #11613) and #9679.Emilio Jesus Gallego Arias
2020-05-14Merge PR #12244: Store the OCaml version used for Coq in vo files.Emilio Jesus Gallego Arias
2020-05-13Adding change log for #8808.Hugo Herbelin
2020-05-13Overlay elpiHugo Herbelin
2020-05-13Documenting notations with both terms and binders.Hugo Herbelin
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-13Merge PR #12293: Fix timestamp of coqchk manpageThéo Zimmermann
2020-05-13Make explicit that UGraph lower bounds are only of two kinds.Pierre-Marie Pédrot
2020-05-13do not re-export ListNotations from Program: kill overlaysAntonio Nikishaev
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-13Merge PR #11828: [obligations] Deprecated flag cleanupGaëtan Gilbert
2020-05-13Centralize the OCaml version-checking function.Pierre-Marie Pédrot
2020-05-13Store the OCaml version used for Coq in vo files.Pierre-Marie Pédrot
2020-05-13Test interleaving of command-line options.Théo Zimmermann
2020-05-13Document the changes regarding the order of command-line options.Théo Zimmermann
2020-05-13Clarify the assignee's role in removing the overlay informationAnton Trunov
2020-05-13Clarify the documentation for merging PRs with overlaysAnton Trunov
2020-05-12Merge PR #12309: Remove documentation of -compile, which was removed in #8690.Clément Pit-Claudel