From cd778dae2c0e19ed97d9b84175c0fc193b99d1a7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 24 Jun 2021 10:14:34 +0200
Subject: [PATCH] Comment.

---
 theories/pretty.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/pretty.v b/theories/pretty.v
index d3d0fff4..24664acc 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -22,6 +22,9 @@ 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
+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 :=
   pretty_N_go_help x (wf_guard (S (N.size_nat x)) N.lt_wf_0 x).
 Global Instance pretty_N : Pretty N := λ x,
-- 
GitLab