UsersDiscussion89 - coq/coq GitHub Wiki
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.
The logic
-
Kernel support for primitive efficient integers (PR #6914).
-
The
match
reduction, as well as theiota
reduction which includes it, are now stronger. Formerly,Eval cbv match in match S O with S n => true | O => false end
was returning(fun _ : nat => true) 0
needing abeta
step further to reach a normal form. Substitution of the variables of a pattern by the arguments of a constructor could become part of thematch
reduction. As another example,Eval lazy match in match 3 with 2 => true | _ => false end
would returnfalse
without requiring thebeta
flag (CEPS #34).
Interfaces
- Highlight differences between successive proof steps with ANSI highlights (color, underline, etc.) (PR #6801).
Notations
-
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).
Tactics
-
Tactics
apply
,rewrite
,destruct
,induction
, etc. based on a different unification algorithm (PR #930 and PR #991). -
New syntax
induction t over m
intended to be more intuitive than the currentinduction t in m |- *
(PR #6836). -
Miscellaneous improvements in regularity of
destruct
andinduction
: -
Removal of
Declare Implicit Tactic
. -
Uniformization of the behavior of the variants of
eauto
(PR #721). -
Opportunities to add new introduction patterns (see PR #410, PR #1003, PR #6705).
-
Model for letting tactic behaviors evolve without breaking compatibility, or at least without breaking it too much (discussion at issue 6043).
A comprehensive list of features for version 8.9
The list of new 8.9 features already integrated is listed here and the one planned for integration are listed here.