diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-10 15:23:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-11 15:55:59 +0200 |
| commit | f20a053364421c6f5691bb02c9015a9db5cbfafe (patch) | |
| tree | 3d8dbbdff6629521ff4d02eb562e1ab9015d0aa0 /CHANGES | |
| parent | 0acaa906367c02c57a6d70dd5d19eaea884b7568 (diff) | |
Notations: advertize that distinct "only parsing"/"only printing" rules work.
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 8 |
1 files changed, 8 insertions, 0 deletions
@@ -33,6 +33,14 @@ Tactic language called by OCaml-defined tactics. - Option "Ltac Debug" now applies also to terms built using Ltac functions. +Changes from 8.8.0 to 8.8.1 +=========================== + +Notations + +- Fixed unexpected collision between only-parsing and only-printing + notations (issue #7462). + Changes from 8.8+beta1 to 8.8.0 =============================== |