Highlights

• Sort polymorphism makes it possible to share common constructs over Type, Prop and SProp.
• The notation term%_scope to set a scope only temporarily (in addition to term%scope for opening a scope applying to all subterms).
• lazy, simpl, cbn and cbv and the associated Eval and eval reductions learned to do head reduction when given flag head.
• New Ltac2 APIs, improved Ltac2 exact and dynamic building of Ltac2 term patterns.
• New performance evaluation facilities: Instructions to count CPU instructions used by a command (Linux only) and Profiling system to produce trace files.
• New command Attributes to assign attributes such as deprecated to a library file.

Changes

See the changelog in the reference manual for detailed changes, potential breakages and credits.

Installation Instructions

The base proof assistant can be installed as an opam switch with the following commands:

opam update
opam switch create 4.14.1
opam install coq.8.19.2

Refer to the general install instructions for more information.

Source Distribution

• Source tarball (.tar.gz) for compilation under Unix (including Linux and macOS X) and Microsoft Windows (including Cygwin).
• Also available in .zip format.
• Opam is a source-based distribution of OCaml, Rocq and many companion libraries and tools. Compilation and installation are automated by powerful package managers.
• The official development repo is hosted on GitHub.