aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
2020-04-29Remove dead user-facing code in scheme generation.Pierre-Marie Pédrot
2020-04-29CI: ext-lib is at coq-community nowAntonio Nikishaev
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
2020-04-28[doc] [sphinx] Be silent when running latexmkEmilio Jesus Gallego Arias
2020-04-28[doc] [sphinx] Run in silent mode by defaultEmilio Jesus Gallego Arias
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
2020-04-28Merge PR #12164: Stop relying on side-effects for recursive scheme declarationEmilio Jesus Gallego Arias
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
2020-04-28Merge PR #12003: Improve error messages for Set and Unset commands.Emilio Jesus Gallego Arias
2020-04-28Merge PR #12188: Do not delay the loading of the library_disk field when requ...Emilio Jesus Gallego Arias
2020-04-28Merge PR #12189: Fix an ordering bug in the CODEOWNERS file following #11529.Emilio Jesus Gallego Arias
2020-04-28Close files in fetch_delayedGaëtan Gilbert
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-27[ci] Add coq-tools to the CIJason Gross
2020-04-27Merge PR #12073: Split off Nsatz tactic part into Nsatz_tacticPierre-Marie Pédrot
2020-04-27Merge PR #12175: Calculation speed of Cauchy realsMichael Soegtrop
2020-04-27Merge PR #12160: CoqIDE: Avoid invalidation of an iterator in insert callbackPierre-Marie Pédrot
2020-04-27Merge PR #12168: [dune] Fix dependencies of refman.Emilio Jesus Gallego Arias
2020-04-27Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in...Clément Pit-Claudel
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
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
2020-04-27Merge PR #12181: Add sphinx-clean option to force full sphinx rebuildThéo Zimmermann
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
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
2020-04-26Document the signing procedure of released binary packages.Pierre-Marie Pédrot
2020-04-26constructive square rootVincent Semeria
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
2020-04-26Merge PR #12178: Fix recursively vs corecursively defined messagePierre-Marie Pédrot
2020-04-25Fix recursively vs corecursively defined messageTej Chajed
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
2020-04-25Merge PR #12173: CoqIDE: Revert overzealous application of language-based hig...Pierre-Marie Pédrot
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24[nsatz] Use Export rather than IncludeJason Gross
2020-04-24Add memory stats to tables by defaultJason Gross
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
2020-04-24CoqIDE: Revert overzealous application of language-based highlighting in #12169.Hugo Herbelin
2020-04-24[dune] Fix dependencies of refman.Théo Zimmermann
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann