UsersDiscussion88
This page collected a list of pages dedicated to discuss changes for Coq version 8.8.
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.
- Removal of (implicit) support for template polymorphism since it can be simulated using (explicit) universe polymorphism and thanks to cumulativity propagated through inductive definitions (discussion at PR #889).
-
New strategy based on open scopes for deciding which notation to use among several of them (discussion at PR #873) (initially planned for 8.8 but postponed).
Typical questions are: should abbreviations (i.e. notations bound to a name rather than to a
" ... "grammar rule) support being attached to a scope. What should be their priority relatively to notations defined in a scope for printing. -
Factorizing "match" clauses with same right-hand side (discussion at PR #978).
-
Support for custom alternative grammars for terms (discussion at PR #6247).
-
Tactics
apply,rewrite,destruct,induction, etc. based on a different unification algorithm (postponed to 8.9, discussion at PR #930 and PR #991). -
Removal of
Declare Implicit Tactic(postponed to 8.9).
The list of new 8.8 features that have been integrated is listed here.
To the extent possible under law, the contributors of “Cocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.
By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.