aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-29Merge PR #12195: [doc] [sphinx] Run in silent mode by defaultThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Merge PR #12174: [ci] Add coq-tools to the CIThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29Merge PR #12203: [ci] [doc] misspelled script name create_overlays.shThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
Ack-by: ejgallego Ack-by: ppedrot
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
This is actually supported by Sphinx directly.
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
The convention in the dune build is to be silent except for warnings and errors, so they don't go unnoticed. We could have this controlled by a variable if needed (likely would require some support from Dune?) Solves part of #12194
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: jfehrle
2020-04-28Merge PR #12164: Stop relying on side-effects for recursive scheme declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-28Add comment about decide equality dependence computation.Pierre-Marie Pédrot
2020-04-28Return an option in lookup_scheme.Pierre-Marie Pédrot
2020-04-28Stop relying on side-effects for recursive scheme declaration.Pierre-Marie Pédrot
Instead, we register functions dynamically declaring the dependencies of the scheme to be generated. We had to fix the test-suite because an internal scheme name changed. We could also tweak the internal flag of scheme dependencies, but in this particular case it looks more like a bug from the previous implementation.
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: jfehrle
2020-04-28Merge PR #12188: Do not delay the loading of the library_disk field when ↵Emilio Jesus Gallego Arias
requiring libraries Reviewed-by: ejgallego
2020-04-28Merge PR #12189: Fix an ordering bug in the CODEOWNERS file following #11529.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-28Close files in fetch_delayedGaëtan Gilbert
Close #12192 Also removed transforming arbitrary exceptions into Faulty to make it easier to reason about exception flow
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-27[ci] Add coq-tools to the CIJason Gross
After #12023 broke the bug minimizer, I'd like to add [coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's relatively light-weight (under 5 minutes, I believe), and I'd like to know when it's going to break on master before it's broken, rather than after. It tests a relatively under-tested part of Coq, mostly (the display output of error message, by and large), and I'm happy to take responsibility for fixing it when some PR is going to break it (mainly I just want a sort-of early warning system, and I want PRs to not accidentally break it by changing things that they don't realize they're changing).
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
Reviewed-by: anton-trunov Reviewed-by: ppedrot
2020-04-27Merge PR #12175: Calculation speed of Cauchy realsMichael Soegtrop
Reviewed-by: MSoegtropIMC
2020-04-27Merge PR #12160: CoqIDE: Avoid invalidation of an iterator in insert callbackPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-27Merge PR #12168: [dune] Fix dependencies of refman.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-27Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed ↵Clément Pit-Claudel
in 8.5).
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
Reviewed-by: vbgl
2020-04-27Fix an ordering bug in the CODEOWNERS file following #11529.Théo Zimmermann
2020-04-27Do not delay the loading of the library_disk field when requiring libraries.Pierre-Marie Pédrot
The reason for which the code was written this way is probably historical. In the current implementation, we read the marshalled data exactly once by library, thus there is no gain from delaying.
2020-04-27Merge PR #12181: Add sphinx-clean option to force full sphinx rebuildThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-27Further documentation improvements.Théo Zimmermann
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-26Add sphinx_clean option to force full sphinx rebuildJim Fehrle
2020-04-26Merge PR #12092: Implement a name-based representation for vo files.Enrico Tassi
Reviewed-by: ejgallego Ack-by: gares
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-26constructive square rootVincent Semeria
Convert into a performance test Put time bound at the beginning of file Add Time command in the test
2020-04-26Open object files in binary mode.Pierre-Marie Pédrot
2020-04-26Tweak a comment on the low-level objfile API.Pierre-Marie Pédrot
2020-04-26Move the ObjFile module to its own file.Pierre-Marie Pédrot
2020-04-26Implement a name-based representation for vo files.Pierre-Marie Pédrot
See CEP#44 for futher details.
2020-04-26Merge PR #12178: Fix recursively vs corecursively defined messagePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-25Fix recursively vs corecursively defined messageTej Chajed
Closes #12177.
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
This makes it show the shape of the induction hypothesis in the second goal instead of just saying "subgoal 2 is S n <= S n".
2020-04-25Merge PR #12173: CoqIDE: Revert overzealous application of language-based ↵Pierre-Marie Pédrot
highlighting from #12169 Reviewed-by: ppedrot
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24[nsatz] Use Export rather than IncludeJason Gross
As per https://github.com/coq/coq/pull/12073#issuecomment-612869336
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-24CoqIDE: Revert overzealous application of language-based highlighting in #12169.Hugo Herbelin
The parsing rules defining classes of lexemes in language configuration expect a Coq document and are not relevant in the message and proof window. Thus backtracking on this part of #12169. Keeping the highlighting style though.
2020-04-24[dune] Fix dependencies of refman.Théo Zimmermann
Dependencies specified through an alias do not trigger a rebuild when they are modified. This is likely a Dune bug, but we still need to fix this on our side as this is inconvenient.
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-23Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: gares
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 23:18:44 +0000