aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Merge PR #12217: Fix #12215: ci scripts naming inconsistenciesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-01Merge PR #12222: Less confusing configure message when lablgtk exists but ↵Emilio Jesus Gallego Arias
not lablgtksourceview Reviewed-by: ejgallego
2020-04-30Less confusing configure message when lablgtk exists but not lablgtksourceview.Hugo Herbelin
2020-04-30Merge PR #12213: [zify] add support for Nat.le, Nat.lt and Nat.eqVincent Laporte
Reviewed-by: vbgl
2020-04-30renaming in Makefile.ci and ci scripts to avoid inconsistenciesOlivier Laurent
2020-04-30Merge PR #12216: Remove outdated code and comments in Declare.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-30[zify] add support for Nat.le, Nat.lt and Nat.eqFrédéric Besson
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat. The required declarations are now added in ZifyInst.
2020-04-30Merge PR #12107: Remove mod_constraints field of module bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-04-30Remove outdated code and comments in Declare.Pierre-Marie Pédrot
Some comments referred to the old way of redeclaring constants at section closure. One of the comments was almost 20 years old...
2020-04-30Merge PR #12208: Reduce rational numbers in Cauchy real addition, to ↵Michael Soegtrop
accelerate it Reviewed-by: MSoegtropIMC
2020-04-29Merge PR #12209: Merge duplicates in .mailmapThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: rnrand
2020-04-29Merge duplicates in .mailmapJason Gross
I gave preference to the email address with the larger number of commits. To find duplicates, I used the script ```bash for i in $(git shortlog -nse | sed s'/^\s*[0-9]*\s*//g' | grep -o '^[^<]*' | sed s'/\s*$//g' | sed s'/ /,/g'); do if [ $(git shortlog -nse | sed s'/ /,/g' | grep -c "$i") -gt 1 ]; then git shortlog -nse | grep "$(echo "$i" | sed s'/,/ /g')"; fi; done ```
2020-04-29Reduce rational numbers in Cauchy real addition, to accelerate itVincent Semeria
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12027: Fix #3415: coqdoc links projections rather than constructor ↵Emilio Jesus Gallego Arias
in record tuples Reviewed-by: ejgallego
2020-04-29Merge PR #12198: CI: change ext-lib url, it is at coq-community nowEmilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-04-29Merge PR #12202: Centralize the call to `tclEFFECTS` in scheme declarationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ↵Clément Pit-Claudel
index Ack-by: Zimmi48
2020-04-29Merge PR #12158: [univ] API to demote global universesMatthieu Sozeau
Reviewed-by: mattam82
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-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-29Merge PR #12203: [ci] [doc] misspelled script name create_overlays.shThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-29[univ] API to demote global universesEnrico Tassi
2020-04-29correct script name create_overlays.shOlivier Laurent
2020-04-29Merge the call to tclEFFECTS into find_scheme.Pierre-Marie Pédrot
This encapsulates better the invariants of this function.
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-29CI: ext-lib is at coq-community nowAntonio Nikishaev
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:14:59 +0000