UsersDiscussion88 - coq/coq GitHub Wiki

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.