aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-02-01No spaces with em-dashes.Théo Zimmermann
Co-Authored-By: Jason Gross <jasongross9@gmail.com>
2020-01-31Clarify expectations for overlays in contributing guide and CI doc.Théo Zimmermann
Contributors are *not* required to prepare all the patches by themselves. They can request help from project authors, who should be ready to take part in this. Also, finish replacing "development" by the more appropriate word "project".
2020-01-31[contributing guide] Clarify some subtitles.Théo Zimmermann
2020-01-23Merge PR #11446: Changed Gitlab CI runner tag for Windows to windows-inriaEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-01-23Changed Gitlab CI runner tag for Windows to windows-inriaMichael Soegtrop
2020-01-23Merge PR #11444: Minor tweaks to the 8.11 changelog.Pierre-Marie Pédrot
Reviewed-by: jfehrle
2020-01-23Merge PR #11445: Clear patches folder before each windows build runThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-23More minor tweaks to the 8.11 changelog.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-23Add missing 'and'.Théo Zimmermann
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-01-22Clear patches folder before each windows build runMichael Soegtrop
2020-01-22Minor tweaks to the 8.11 changelog.Théo Zimmermann
2020-01-22Merge PR #11372: Changelog for 8.11.0.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-22Merge PR #11438: [lint] Use makefile wrapper instead of calling dune command ↵Théo Zimmermann
directly. Reviewed-by: Zimmi48
2020-01-22Insert changelog entry for #11430 from v8.11 branch.Théo Zimmermann
2020-01-22[lint] Use makefile wrapper instead of calling dune command directly.Emilio Jesus Gallego Arias
This is necessary until we get of the voboot step. See https://github.com/coq/coq/pull/11406#issuecomment-577261843 for more details.
2020-01-22Move new entries in 8.11.0 changelog.Théo Zimmermann
2020-01-22A few edits to the 8.11 section of the Changes chapter.Théo Zimmermann
- Mention Guillaume Claret among maintainers of the OPAM repository (as suggested by Karl Palmskog). - Update links to the documentation to avoid being outdated. - Mention sections beyond the one on 8.11+beta1.
2020-01-22Changelog for 8.11.0.Théo Zimmermann
2020-01-22Merge PR #11422: Fix #11421 computation of Set+2Pierre-Marie Pédrot
Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-22Merge PR #11433: [xml-protocol doc] Fix link to vscoqHugo Herbelin
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-01-21[xml-protocol doc] Fix link to vscoqRamkumar Ramachandra
2020-01-21Merge PR #11425: Miscellaneous typosThéo Zimmermann
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-01-21Merge PR #11431: [ci] Pin SF until they solve their CI issues.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-21[ci] Pin SF until they solve their CI issues.Emilio Jesus Gallego Arias
Latest build on SF is erroring due to: ``` "messages" : [ { "type" : "error", "message" : "This job has been blocked because no credits are available on your plan. Please upgrade to continue building.", "reason" : "execution-authorization-failed" } ], ``` we temporary pin to the last successful job that produced artifacts.
2020-01-21Translating a comment from French to English.Hugo Herbelin
2020-01-21Typo in an anomaly message.Hugo Herbelin
2020-01-21Typo in a comment of univ.mli.Hugo Herbelin
2020-01-21Reference manual: Typos/English in chapter universe polymorphism.Hugo Herbelin
2020-01-20Merge PR #11411: Checker validation now performed over reified dataGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-20Merge PR #11428: [mltop] Deprecate -load-ml options in anticipation of #11409Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2020-01-20[mltop] Deprecate -load-ml options in anticipation of #11409Emilio Jesus Gallego Arias
2020-01-19Merge PR #11406: [dune] [dbg] Add support for coqtop in dune-dbgGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-01-19Merge PR #11214: Add a script to pin CI developments.Gaëtan Gilbert
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-19Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors ↵Pierre-Marie Pédrot
cons and nil Reviewed-by: Zimmi48 Reviewed-by: herbelin Reviewed-by: ppedrot
2020-01-19Merge PR #11348: Discharge inductive types without rechecking themPierre-Marie Pédrot
Ack-by: maximedenes Reviewed-by: ppedrot
2020-01-19Removing text saying XML is future of PG, adding explicitly vscoq as a userHugo Herbelin
2020-01-17Merge PR #11413: [doc] [ltac2] Build Ltac2 documentationThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-17Merge PR #11410: [ci] [gitlab] Add `interruptible: true` to jobs.Théo Zimmermann
Reviewed-by: Zimmi48
2020-01-17Fix issue #11396 : Rlist hides standard list constructors cons and nilMichael Soegtrop
2020-01-17[doc] [ltac2] Build Ltac2 documentation [make build system]Emilio Jesus Gallego Arias
Build and install the Ltac2 documentation.
2020-01-17[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]Emilio Jesus Gallego Arias
This partially fixes #10139 ; we now build the Ltac2 documentation and deploy it. The fix here can be used for inspiration to do the make-based part.
2020-01-17[dune] [dbg] Add support for coqtop in dune-dbgEmilio Jesus Gallego Arias
We also workaround problem #11405 , however, this should be reverted once the problem is fixed in OCaml upstream.
2020-01-17[ci] [gitlab] Add `interruptible: true` to jobs.Emilio Jesus Gallego Arias
When a newer pipeline contains the same job, the job can be interrupted, see: https://docs.gitlab.com/ee/ci/yaml/README.html#interruptible This should help with job limits (c.f. #11320 ) The patch is a bit unsatisfactory due to the duplication needed; we could define a base job and use extends, but not sure it is worth it for now.
2020-01-17Merge PR #11362: Lia bugfix 11191Maxime Dénès
Reviewed-by: maximedenes
2020-01-16Merge PR #11400: Use the GTK completion widget in CoqIDEEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-01-16Adding a changelog.Pierre-Marie Pédrot
2020-01-16Adding an option to change the autocompletion delay.Pierre-Marie Pédrot
2020-01-16Better handling of asynchronous completion.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:59:02 +0000