Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
This page collects a list of pages dedicated to discuss changes planned in Coq version 8.9.
Users are welcomed to comment and discuss with developers on these changes at the indicated pages, or by adding a new issue page if no link already exists.
See also the 8.9 roadmap page for an upstream perspective at the 8.9 projects.
Kernel support for primitive efficient integers (PR #6914).
matchreduction, as well as the
iotareduction which includes it, are now stronger. Formerly,
Eval cbv match in match S O with S n => true | O => false endwas returning
(fun _ : nat => true) 0needing a
betastep further to reach a normal form. Substitution of the variables of a pattern by the arguments of a constructor could become part of the
matchreduction. As another example,
Eval lazy match in match 3 with 2 => true | _ => false endwould return
falsewithout requiring the
betaflag (CEPS #34).
- Highlight differences between successive proof steps with ANSI highlights (color, underline, etc.) (PR #6801).
User-level support for declaring numeral notations for arbitrary types (PR #496).
Support for custom alternative grammars for terms (PR #6247).
New strategy based on open scopes for deciding which notation to use among several of them (PR #873).
New command for explicit declaration of a scope, intended to be eventually mandatory (PR #7135).
New semantics to
Set Printing All: it can be combined with other printing options for better customization (PR #6560).
induction t over mintended to be more intuitive than the current
induction t in m |- *(PR #6836).
Miscellaneous improvements in regularity of
Declare Implicit Tactic.
Uniformization of the behavior of the variants of
Model for letting tactic behaviors evolve without breaking compatibility, or at least without breaking it too much (discussion at issue 6043).