Releases

• Reenable support for native_compute when compiled with OCaml 5. As it relies on some architecture-specific code, only some x86 setups are supported for now
• Records in Type and Prop, with only fields in SProp, can now have primitive projections but without eta conversion.
• Implicit elaboration of elimination constraints
• Parsing of elimination constraints in prenex polymorphic definitions as well as in constraints declaration Constraint s1 -> s2.
• Induction hypotheses are now generated for nested arguments provided an All predicate, and a theorem to prove it, have been registered with the keys All and AllForall.
• Add a Scheme All command to generate the All predicate and its theorem for inductive types used for the eliminators of nested inductive types
• Tactics such as induction find eliminators (like nat_rect) through the Register Scheme table (which is automatically populated by Scheme and automatic scheme declarations) instead of by name (the lookup by name remains for now for backward compatibility)
• attribute schemes to control automatic scheme declaration.
• Goal names can be automatically generated for induction, destruct and eapply by using the Generate Goal Names flag
• congruence tactics now handle primitive ints, floats and strings
• Ltac2 Custom Entry making it possible to define more complex Ltac2 Notations and many other additions to Ltac2 (see below for details).
• Printing Fully Qualified to print all names (global references, modules, module types, universes, etc) using fully qualified paths
• Generalized universe polymorphism flag structure (ML API change)

• For Rocq 9.0
• Coq 8.12.2-8.20.1 available

• Added theory of modular integer arithmetic
• Enhancements of nsatz
• Deprecation of Rtauto (looking for maintainer)

• Fixed incorrect guard checking leading to inconsistencies
• Sort polymorphic universe instances should now be written as @{s ; u} instead of @{s | u}
• Fixed handling of notation variables for ltac2 in notations (i.e. Notation "'foo' x" := ltac2:(...))
• Support for refine attribute in Definition
• Rocq can be compile-time configured to be relocatable
• Extraction handles sort polymorphic definitions
• Fixed an anomaly when defining a sort polymorphic inductive without enabling Universe Polymorphism.
• Fixed compatibility with OCaml 5.4 with warnings as errors

• For Rocq 9.0
• Coq 8.12.2-8.20.1 available

• For Rocq 9.0
• Coq 8.12.2-8.20.1 available

• Fixed incorrect guard checking leading to inconsistencies
• Sort polymorphic universe instances should now be written as @{s ; u} instead of @{s | u}
• Fixed handling of notation variables for ltac2 in notations (i.e. Notation "'foo' x" := ltac2:(...))
• Support for refine attribute in Definition
• Rocq can be compile-time configured to be relocatable
• Extraction handles sort polymorphic definitions

Changed the requirement prefix of the standard library from Coq to Stdlib and made it mandatory.

• A single command line tool: rocq
• Compatibility Coq binaries and packages
• Improvements to template and sort polymorphism
• Support for quick fixes in LSP-based interfaces (e.g. for deprecations)

• For Coq 8.20.1
• Coq 8.12.2-8.19.0 available

• A single command line tool: rocq
• Compatibility Coq binaries and packages
• Improvements to template and sort polymorphism
• Support for quick fixes in LSP-based interfaces (e.g. for deprecations)

• various bugfixes

• For Coq 8.19.2
• Coq 8.12.2-8.18.0 available
• Compatibility with opam 2.3.0

• 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.

• User-defined rewrite rules
• Primitive strings
• A lot of work went into reducing the size of the bytecode segment, which in turn means that .vo files might now be considerably smaller.
• A new version of the docker-keeper compiler to build and maintain Docker images of Coq.