diff --git a/theories/pretty.v b/theories/pretty.v index 24664acc35c6b307bc14cf4e35f2c2f315203b5e..f5ea9a339c61a609c55a8806131ea2cebb2c46da 100644 --- a/theories/pretty.v +++ b/theories/pretty.v @@ -22,7 +22,7 @@ Fixpoint pretty_N_go_help (x : N) (acc : Acc (<)%N x) (s : string) : string := (String (pretty_N_char (x `mod` 10)) s) | right _ => s end. -(* The argument [S (N.size_nat x)] of [wf_guard] makes sure that computation +(** The argument [S (N.size_nat x)] of [wf_guard] makes sure that computation works if [x] is a closed term, but that it blocks if [x] is an open term. The latter prevents unexpected stack overflows, see [tests/pretty.v]. *) Definition pretty_N_go (x : N) : string → string :=