Hugo Herbelin edited this page Apr 5, 2018 · 4 revisions

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.

The logic

  • 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).

A comprehensive list of features for version 8.8

The list of new 8.8 features that have been integrated is listed here.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.