PrincetonUniversity/VST

Bad pretty-printing for `->`

Closed this issue · 1 comments

QinshiWang commented

Without importing VST,

Lemma foo : nat -> nat.

It prints

1 goal
______________________________________(1/1)
nat -> nat

After importing VST,

Require Import VST.floyd.proofauto.
Lemma foo : nat -> nat.

It prints

1 goal
______________________________________(1/1)
nat->nat

Version

VST commit 8ff48be
Coq 8.15.1

andrew-appel commented

See Coq issue 16262, referenced just above. It's caused by floyd/Clightnotations.v, the Notation "p_val -> f_val" command. It could perhaps be fixed by removing the "format" specifier from that line, assuming that fix doesn't break anything else.