diff --git a/tests/pretty.v b/tests/pretty.v
index 8557d8fe23b08aa26ac94d9d74564d48e6456eea..6bb0768fce926b6a083e3a8f4b6abb633be0f69c 100644
--- a/tests/pretty.v
+++ b/tests/pretty.v
@@ -1,4 +1,5 @@
 From stdpp Require Import pretty.
+From Coq Require Import Ascii.
 
 Section N.
   Local Open Scope N_scope.
@@ -17,6 +18,17 @@ Section N.
   Proof. reflexivity. Qed.
 End N.
 
+(** Minimized version of:
+
+  https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E
+
+Fixed by making the [wp_guard] in [pretty_N_go] proportional to the
+size of the input so that it blocks in case the input is an open term. *)
+Lemma test_no_stack_overflow p n :
+  get n (pretty (N.pos p)) ≠ Some "_"%char →
+  get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
+Proof. intros Hlem. apply Hlem. Qed.
+
 Section nat.
   Local Open Scope nat_scope.
 
diff --git a/theories/pretty.v b/theories/pretty.v
index 7ba38b338b0d71004c7944b7fe69a25f9ab6ddaa..f5ea9a339c61a609c55a8806131ea2cebb2c46da 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -22,8 +22,11 @@ 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 32 N.lt_wf_0 x).
+  pretty_N_go_help x (wf_guard (S (N.size_nat x)) N.lt_wf_0 x).
 Global Instance pretty_N : Pretty N := λ x,
   if decide (x = 0)%N then "0" else pretty_N_go x "".