aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Update release-process.mdEnrico Tassi
2020-05-18Merge PR #12346: Update to 8.13.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-18Update to 8.13.Théo Zimmermann
Part of this PR was automatically generated by running dev/doc/update-compat.py --master
2020-05-18Merge PR #11980: Improve spacing in Print AssumptionsEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: herbelin
2020-05-18Merge PR #12341: [search] [ssr] Emit deprecated message when calling search ↵Théo Zimmermann
from ssreflect Reviewed-by: Zimmi48 Ack-by: gares
2020-05-18Merge PR #12345: test-suite/Makefile: fix incomplete prerequisite listEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
but ssrsearch is not loaded. Fixes #12338
2020-05-18test-suite/Makefile: fix incomplete prerequisite listGaëtan Gilbert
2020-05-18Improve spacing in Print AssumptionsGaëtan Gilbert
cf "If this is implemented, long names might cause a printing problem:" in #11852
2020-05-17Merge PR #11981: Ltac2: add notations for eval cbv in ... and other in place ↵Jason Gross
reductions Reviewed-by: JasonGross Ack-by: Zimmi48
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
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-16Merge PR #12071: [ci] [micromega] Fix windows build and Micromega bug ↵Théo Zimmermann
introduced in #11756 Reviewed-by: Zimmi48
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
- use a different mirror for main cygwin archive - (always) publish build log as artifact - fix call to dune makefiles - we do just build Coq for now, as: + dune is rebuilding Coq to run the test-suite, this needs move investigation. + the test suite seems to take long and it times-out on Win.
2020-05-16Revert "Temporarily disable Windows job on Azure."Emilio Jesus Gallego Arias
This reverts commit 646a12b2f4660d6e9d5a812febdccab44221d1f0.
2020-05-16[micromega] Revert bad change from 5001deed21e8f4027411cc6413a9d2b98e1bcceeEmilio Jesus Gallego Arias
Analysis by Jason Gross: > The previous semantics was to reset the file offset to 0 during the > unlock operation, unless it fails, in which case you'd roll back the > file offset to it's present position (and very dubiously not report > any issues). The new semantics say to always roll the file offset > back to it's initial position, meaning that the position is at the > end of the file after unlocking. As far as I can tell, this results > in appending marshelled blobs to the cache file on every call to > add, rather than overwriting the cache file with the marshelled blob > of the updated table. Presumably unmarshelling the concatenation of > marshelled data can result in segfaults somehow? This also explains > why the bug only shows up sometimes; you need to get the system into > a state where it writes to the cache in a way that concatenates > blobs in the right way, but once you have such a cache you'll > segfault every time you read from it. > > I think we should probably assert false in the with block, or just > remove it entirely http://man7.org/linux/man-pages/man3/lockf.3.html > doesn't say anything about lockf erroring on unlocking). If we start > seeing errors, we can turn it into a warning. Closes: #12072
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-16Merge PR #12277: Checking validity of coqdoc file name (fixes #12265)Théo Zimmermann
Reviewed-by: Zimmi48 Ack-by: randomdross
2020-05-16Merge PR #12335: Clarify release-process.mdThéo Zimmermann
Reviewed-by: Zimmi48
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
Error happened only when writing: functional induction f x y z. instead of functional induction (f x y z). Now the former is equivalent to the former: implicits must be omitted. Hence small source of incompatibility, but a more homogeneous behaviour.
2020-05-16Prove that classical reals implement constructive reals. Also move sums, min ↵Vincent Semeria
and max to CoRN. Update stdlib index Remove ConstructiveSum from the index Add changelog entry Make constructive reals experimental
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
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
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
The main use case of SearchHead is now handled by headconcl: The secondary use case was redundant with SearchPattern.
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
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
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
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict match to an hypothesis or the conclusion, possibly only at the head (like SearchHead in this latter case) - new clause "is:" to search by kind of object (for some list of kinds) - support for any combination of negations, disjunctions and conjunctions, using a syntax close to that of intropatterns.
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 ↵Emilio Jesus Gallego Arias
implicit types Reviewed-by: ejgallego
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2020-05-15Clarify release-process.mdEnrico Tassi
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-15Merge PR #11755: [exn] [tactics] improve backtraces on monadic errorsPierre-Marie Pédrot
Ack-by: gares Ack-by: ppedrot
2020-05-15Merge PR #12243: Add a note on build-time dependencies to INSTALL.md.Emilio Jesus Gallego Arias
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: ppedrot
2020-05-15Fix typo.Théo Zimmermann
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 03:20:24 +0000