aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-17Fix proof_diffs_test.mlGaëtan Gilbert
2020-05-17test-suite: fix bug causing unit tests to be skippedGaëtan Gilbert
2020-05-17Ltac2: add notations for eval cbv in ... and other in place reductionsMichael Soegtrop
2020-05-16Merge PR #12288: Prove that classical reals implement constructive reals.Michael Soegtrop
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
2020-05-16Merge PR #12071: [ci] [micromega] Fix windows build and Micromega bug introdu...Théo Zimmermann
2020-05-16Merge PR #12330: Add redirects for HTML pages that were moved.Clément Pit-Claudel
2020-05-16[ci] [azure] Rework windows Azure pipelineEmilio Jesus Gallego Arias
2020-05-16Revert "Temporarily disable Windows job on Azure."Emilio Jesus Gallego Arias
2020-05-16[micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bcceeEmilio Jesus Gallego Arias
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
2020-05-16Merge PR #12277: Checking validity of coqdoc file name (fixes #12265)Théo Zimmermann
2020-05-16Merge PR #12335: Clarify release-process.mdThéo Zimmermann
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 00:45:31 +0000