diff --git a/CHANGELOG.md b/CHANGELOG.md index 14a3d30db6964c4f6910eb537e5ecb8abbd0316b..cf2bd38cf7792d06198518705aecc781a4f5b295 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -228,6 +228,7 @@ Changes: - Use `disj_union` (notation `⊎`) for disjoint union on multisets (that adds the multiplicities). Repurpose `∪` on multisets for the actual union (that takes the max of the multiplicities). +- Set `Hint Mode` for `pretty`. Naming: diff --git a/theories/pretty.v b/theories/pretty.v index c1d6b1c6c681da04a6c0820bb80c3d410bf7a2b4..e1a28d941d372b6c0a87453396aa31f4ad6e4de8 100644 --- a/theories/pretty.v +++ b/theories/pretty.v @@ -4,6 +4,7 @@ From Coq Require Import Ascii. From stdpp Require Import options. Class Pretty A := pretty : A → string. +Hint Mode Pretty ! : typeclass_instances. Definition pretty_N_char (x : N) : ascii := match x with