search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
442 stars 93 forks source link

Bad pretty-printing for `->` #594

Closed QinshiWang closed 2 years ago

QinshiWang commented 2 years ago

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 8ff48be92e1be3df3cc7a1959852935792ba168c Coq 8.15.1

andrew-appel commented 2 years ago

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.