Changes in Coq since the last WG (20181216) - rocq-prover/rocq GitHub Wiki

Changes in Coq since the last WG

From December 16^th^, 2018 to February 3^rd^ 2019

git log --since='2018-12-16' --until='2019-02-03' --pretty=oneline | grep 'Merge PR' | sed -e 's/^.*Merge PR #\([0-9]*\): \(.*\)$/\1: \2/'

9178: CoqIDE: Restoring configuration of default width/height of main window. (Hugo)

9172: Rework proof interface (Emilio)
Maxime did some cleaning and refactoring in the STM (9220, 9219, 9218, 9331, 9263)
9153: Move reduction modules to tactics (Emilio)
Gaëtan did some refactoring in the kernel (9237, 9159)
Gaëtan did some cleaning related to template polymorphism (8488, 9182, 9325)
9139: [engine] Allow debug printers to access the environment (Emilio)
9276: Remove dead code from CClosure (Pierre-Marie)
9027: Refactor checking of inductive types (Gaëtan)
8734: Make diffs work for more input strings (Jim)
Maxime disabled Refine instance Mode by default (9270) and made Instance without a body always open a proof (9274)
9043: [windows] Cleanup cruft from dev/build/windows (Emilio)
9095: [toplevel] Deprecate -compile flag in favor of coqc (Emilio)
9395: Global [open Univ] in UState (Gaëtan)

In the STM, by Enrico (9206, 9335, 9372, 9399), by Gaëtan (9222, 9223), by Maxime (9048), by Emilio (9421)
In automatic introduction, by Jasper (9160)
In notations, by Hugo (9231, 9337, 9214)
In ltac, by Gaëtan (9248)
In printing, by Hugo (9249, 8373)
In pretyping, by Gaëtan (9241)
In interpretation, by Hugo (9292)
In instances, by Maxime (9273), by Jasper (9307)
In coqc and coqtop, by Maxime (9316, 9357)
On MS-Windows, by Michael (9192, 9225)
In universe polymorphism, by Gaëtan (9361)
In canonical structures, by Enrico (9377)
In the checker, by Gaëtan (9250)

8856: Compile Coq with OCaml 4.08 (Emilio)
9215: Set up CI with Azure Pipelines (Gaëtan) (see also 9243, 9318 by Kayla Ngan, 9332)
9081: [dune] A new Makefile.dune target for each package (coq, coqide-server and coqide) (Emilio)
9265: Do not exclude "opened" bugs from report (Maxime)
9278: [ci] Annotate plugins and libraries (Théo)
Exit travis, by Gaëtan (9224, 9383)
9277: [dune] Build refman with fatal warnings like in the Makefile build (Théo)
9088: Add CI job running test suite with async-proofs on (Maxime)
9440: Create deployment environment for Cachix (Théo)

9183: List members of the code of conduct enforcement team (Théo)
9143: Documenting the internal role of to_string and print in Names (Hugo)
Gaëtan improved the commit messages produced by merge-pr (9242, 9353)
9339: Move plugin tutorial to team ownership
Various improvements to the user manual (9374 by Laurent, 9392, 9449 and 9402 by GitHub user akr, 9269 by Jim, 9384 by Théo, 9391 by David A. Dalrymple, 9424 by Ryan Scott, 9435 by Gaëtan).