Release of Rocq 9.2.0
We are happy to announce that Rocq 9.2.0 has been released. The main changes are:
- Reenable support for
native_computewhen 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)
See the changelog Recent changes for more information.
Installation Instructions
The base compiler can be installed as an opam switch with the following commands:
opam update
opam switch create 4.14.1
opam install rocq-prover rocq-core=9.2.0
The source code for the release is also directly available on: