Ana Guerrero
7a59074778
- Update to version 9.2.0.
* 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 Notation`s and many other additions to `Ltac2` (see
documentation 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).
OBS-URL: https://build.opensuse.org/request/show/1343994
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/coq?expand=0&rev=32