aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Merge PR #12289: test-suite: fix bug causing unit tests to be skippedHugo Herbelin
2020-05-18[test-suite] Ensure copies of files are writableEmilio Jesus Gallego Arias
2020-05-18Merge PR #12346: Update to 8.13.Emilio Jesus Gallego Arias
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
2020-05-18Merge PR #12341: [search] [ssr] Emit deprecated message when calling search f...Théo Zimmermann
2020-05-18Direct URL for triggering a pipeline with SKIP_DOCKER=false.Théo Zimmermann
2020-05-18[azure OSX] Export OCAMLPATH so test-suite sees OCaml libsEmilio Jesus Gallego Arias
2020-05-18Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite listEmilio Jesus Gallego Arias
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-18Cleanup: remove noisy "uctx_" prefixes in ustate.mlGaëtan Gilbert
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
2020-05-18Cleanup: remove noisy "sec_" prefixes in section.mlGaëtan Gilbert
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ...Jason Gross
2020-05-17Revert "[test] unit tests for ide/coq_lex.ml" + makefile supportGaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 22:06:17 +0000