• Changes in Coq since the last WG
• Foreword
• Aim
• Methodology
• Performances
• 8708: Pierre-Marie improved the performance of conversion by changing an unfolding heuristic.
• 8841: Pierre-Marie implemented a performance optimization
• 8824: Pierre-Marie improved the performance of the kernel by dropping convertibility checks on domains of pattern branches in pattern-matching
• 8255: Pierre-Marie improved type-checking of application nodes
• Features
• 8870: Maxime updated the -bytecode-compiler and -native-compiler flags of coqc and coqtop
• 8515: Gaëtan redesigned how commands declare and handle their attributes (8515, 8917)
• 8766: Emilio implemented basic support in Nametab for efficient completion
• 8779: Pierre-Marie removed the “implicit tactic” feature
• 8451: Gaëtan added a Subgraph option to the Print Universes command
• 8987: Maxime deprecated hint declaration/removal with no specified database
• 9001: Emilio removed the deprecated option Automatic Introduction
• 8920: Gaëtan deprecated the “Typeclasses Axioms Are Instances” option
• 8890: Hugo improved some interaction between notations and coercions
• 8850: Gaëtan added private universes for opaque polymorphic constants
• 8965: Jason enabled user-defined string notations
• 8811: Gaëtan added EConstr-aware functions to produce kernel entries
• 9015: Vincent added a warning when, in type classes, the RHS of :> is not a class
• Build-system, CI
• Emilio improved the dune-based build-system (8802, 8762, 8744, 8903, 8912, 8901, 8960, 8959, 9035, 8948, 9068, 9106, 9151, 9147)
• Théo improved default.nix (8821, 8836)
• 8711: Emilio improved CI for MS-Windows
• 8868: Vincent updated the Docker image used for CI
• 8918: Gaëtan fixed overlays on Windows CI
• 8927: Kamil Trzciński (from Gitlab) improved performances of CI on gitlab
• Vincent proposed nix helpers for debugging external projects from CI (8978, 9057)
• 9018: Emilio provided a script to automatically setup overlays
• 9033: Gaëtan fixed installation of the stdlib documentation
• 9016: Gaëtan improved the log of failed builds on appveyor
• 9021: Gaëtan improved the merging script
• 9087: Maxime added a job building the stdlib with async-proofs on
• Test suite
• Hugo improved the test-suite (8786, 9193)
• 8655: Vincent made the test-suite run the checker on all generated .vo files
• Documentation
• github user sampablokuper improved the manual (8799, 8798, 8766)
• 8813: Vincent fixed a few rendering issues in the manual
• 8737: Tej Chajed improved a few error messages w.r.t. record fields
• 8851: Matthieu wrote the credits for Coq 8.9
• Théo improved the manual (8845, 9036, 9121, 9196, 9073)
• 8809: Emilio improved the developer’s documentation
• 8884: Guillaume improved the rendering of the credits
• 8926: Théo fixed the CHANGES file
• Théo documented the merging process (8098) and the creation of code owner teams (9053)
• 8408: Enrico improved the HTML rendering of the ssreflect library documentation
• 8894: Gaëtan improved an error message related to polymorphic universes
• 8975: github user soraros improved the documentation of the micromega tactics
• 8911: Jim ensured that all flags and options are documented
• 9150: Emilio enabled the “incorrect doc comment” warning and fixed comments accordingly
• Standard library
• 8365: 李弈帥 (Yishuai Li) contributed the ByteVector type to the Strings library
• 8812: Vincent made ssreflect use Coqlib
• 8815: 李弈帥 (Yishuai Li) contributed lemmas about numbers and vectors
• 8888: Vincent Semeria proved that the set of real numbers is uncountable
• 8807: Larry Darryl Lee Jr. added two lemmas to the List library
• 7221: 李垚 (Yao Li) implemented the OrderedTypeEx interface for strings
• Refactoring
• Hugo performed some cleaning in the kernel
• 8707: Pierre-Marie separated the kernel implementation for the term cache and its reuse in the out-of-kernel CBV reduction, allow[ing] for further cleanups of static or unused data
• 8777: Pierre-Marie cleaned the side-effects API, moving it into Safe_typing
• 8753: Emilio made config a “proper” library
• 8684: Maxime did some cleaning in the kernel
• 8825: Emilio moved object_name into Libobject
• 8688: Hugo made the evar_map printers from Termops take an environment as arguments
• 8844: Gaëtan moved the abstract tactical to its own module
• 8871: Emilio moved a few functions from Libnames to Nametab
• 8773: Maxime refactored the checker
• Emilio renamed Vernacinterp to Vernacextend (8919, 9003)
• 8914: Emilio decoupled CoqProject_file and Feedback
• 8902: Emilio added CAst.t nodes into the tactic AST
• 7925: Pierre-Marie moved Names.transparent_state to its own module TransparentState
• 8982: Emilio improved the control of “open proof” exceptions
• 8929: Gaëtan refactored liftings
• Emilio refactored the toplevel
• 8705: Emilio turned hooks into optional arguments
• 9169: Emilio ported rtauto and auto to the new proof engine
• CoqPP
• Pierre-Marie worked on coqpp
• 8667: Emilio derived gramlib from Daniel de Rauglaudre’s camlp5 (8667, 9023, 9064, 9065)
• 8843: Gaëtan removed .ml4 files from coqIDE sources
• Pierre-Marie removed the deprecated Token module and dead-code from gramlib (8899, 8907, 8915, 9069)
• Pierre-Marie ported the parser to the type-safe API of Camlp5 (introduced in version 7.06) (8923), but reverted this change (8944) and made it again (9051)
• Gaëtan fixed CoqMakefile w.r.t. .mlg dependencies (8966)
• Emilio and Gaëtan changed the make-based build-system to pack and link gramlib (8985, 9074)
• 8945: Emilio finally removed all dependencies to Camlp5
• 9127: Pierre-Marie remover leftover code that used to handle ml4 files
• Cleaning
• 8741: Matthieu improved the handling of evars in type-classes
• 8780, 8781: Gaëtan performed some cleaning w.r.t. projections
• 8864: Maxime removed many calls to Environ.empty_env
• 8752: Gaëtan removed fragile pattern matching in CClosure
• 8852: Matthieu cleaned the handling of obligation evars
• 8866: Gaëtan added a check for universe instances in Typing
• 8889: Matthieu improved “Program” hooks
• 8760: Gaëtan improved the printing of universe names
• 7881: Github user whitequark reimplemented Store using Dyn
• Emilio removed the cook_proof and start_proof stubs from Pfedit (8999, 9002)
• 9017: Jim removed undocumented options for profiling in ssreflect
• 8998: Emilio removed the Proof_type module
• 9046: Gaëtan made the Goptions.declare_* functions return unit
• 9072: Maxime cleaned the STM flags
• 9102: Emilio removed some aliases from Tacexpr
• 8096: Maxime enhanced the libobject API
• 9172: Emilio reworked the proof interface
• Bug fixes
• Hugo fixed bugs in notations (8806, 8867, 8187)
• Guillaume fixed bugs in CoqIDE (8803, 8804)
• Matthieu fixed a type-classes bug (8849)
• Pierre-Marie fixed a bug in Ltac (8759)
• Emilio fixed an anomaly in printing (8834)
• Hugo fixed a bug related to tactic-in-terms and notation scopes (8745)
• Gaëtan fixed a few bugs in the checker (8877, 8882, 8874, 8996)
• Pierre-Marie fixed an algorithmic issue in the vernac guardedness checker (7952)
• Enrico made the ssreflect dispatch intro pattern stricter (8856)
• Enrico reverted 7936: “Do not allow spliting in res_pf, this is reserved for pretyping” (8934)
• Jasper Hugunin made the behavior of “Automatic Introduction” more uniform (8820)
• Maxime fixed the substitution of inline global reference in tactics (8972)
• Pierre-Marie improved the handling of bound universe names (8601)
• Hugo fixed the grounding of open terms in fixpoints (8892)
• Gaëtan fixed bugs related to universes (8936, 8854, 8974)
• Vincent fixed the VM compilation of int31 eliminators (8886)
• Enrico fixed typeclasses resolution in case/elim patterns (8955)
• Gaëtan fixed the top name in CoqIDE (8991)
• Hugo fixed a few issues in CoqIDE (8968)
• Enrico fixed some race in the stm (8712)
• Gaëtan made the Init module not exported (9013)
• Jim fixed bugs in proof diffing (8967, 9101)
• Gaëtan prevented redeclaration of constraints in Include (8995)
• Maxime fixed a race condition triggered by fresh universe generation (9155)
• Hugo fixed the debug printers: gramlib needs Loc (9197)
• Hugo fixed a warning that was too often raised
• Other PRs merged in the period