aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-16Fix note on implicit arguments in doc of functional induction.Théo Zimmermann
2020-05-16Fix #11761: Functional Induction throws unrecoverable error.Pierre Courtieu
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ...Vincent Semeria
2020-05-16Add redirects for HTML pages that were moved.Théo Zimmermann
2020-05-16Merge PR #11566: [misc] Better preserve backtraces in several modulesPierre-Marie Pédrot
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into mul...Clément Pit-Claudel
2020-05-15Changelog entries for #8855.Théo Zimmermann
2020-05-15Test new Search features.Théo Zimmermann
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Deprecate SearchHead.Théo Zimmermann
2020-05-15Add overlays for coqhammer and coq-dpdgraph.Hugo Herbelin
2020-05-15Moving interpretation of Search commands to their own file: comSearch.ml.Hugo Herbelin
2020-05-15Update dev/doc/release-process.mdEnrico Tassi
2020-05-15Cleaning the use of pstate and evar_map in Search.Hugo Herbelin
2020-05-15Search: Displaying the "use About" notice only when really needed.Hugo Herbelin
2020-05-15Move SSR's Search to a new plugin and deprecate it.Théo Zimmermann
2020-05-15Addressing a suggestion from Théo Zimmermann.Hugo Herbelin
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-15Renaming search_about_item into search_item.Hugo Herbelin
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
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-15Clarify release-process.mdEnrico Tassi
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-15Fix typo.Théo Zimmermann
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-15[interp] Register printers for InternalizationError instead of ad-hoc hanlding.Emilio Jesus Gallego Arias
2020-05-15[misc] Better preserve backtraces in several modulesEmilio Jesus Gallego Arias
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-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Thé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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:33:35 +0000