aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-29Remove dead user-facing code in scheme generation.Pierre-Marie Pédrot
It was trying to warn the user about missing schemes. Since find_scheme was generating those constants anyways, this was never reached.
2020-04-28Merge PR #12193: Close files in fetch_delayedEmilio Jesus Gallego Arias
Ack-by: ejgallego Ack-by: ppedrot
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-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
2020-04-23Merge PR #12120: Fixing #12119 : remove useless hypothesis in ↵Hugo Herbelin
NoDup_Permutation_bis Reviewed-by: herbelin
2020-04-23[documentation] ssreflect: Abbreviations do not support scopeKenji Maillard
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-23Merge PR #12130: [declare] [tactics] Move declare to `vernac`Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-23Fix coq snippets in Tactics chapter.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 04:36:22 +0000