Skip to content
Snippets Groups Projects

Set `Hint Mode` for `pretty`.

Merged Set `Hint Mode` for `pretty`.
robbert/pretty_hint_mode into master
Merged Robbert Krebbers requested to merge robbert/pretty_hint_mode into master
Compare
and
2 files
+ 2
− 0
Compare changes
  • Side-by-side
  • Inline
Files
2
theories/pretty.v
+ 1
− 0
@@ -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