aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-01-28Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml'sPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11419: schemes: use rigid universesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-28Merge PR #11459: cleanup: Lib.freeze doesn't use its [~marshallable] argumentMaxime Dénès
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes
2020-01-27cleanup: Lib.freeze doesn't use its [~marshallable] argumentGaëtan Gilbert
2020-01-27Merge PR #11415: Remove the CoqIDE "Revert all Buffers" command.Hugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin
2020-01-27schemes: use rigid universesGaëtan Gilbert
so for instance ~~~coq Set Printing All. Set Printing Universes. Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= . Lemma bla@{u v|u < v} : foo@{u v} -> False. Proof. induction 1. Qed. ~~~ works.
2020-01-25Merge PR #11025: Add Set NativeCompute TimingMaxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: maximedenes
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 16:09:05 +0000