From 3774c94b70fa872bea6ea585b62041b8cec82348 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Aug 2016 15:29:47 +0200
Subject: [PATCH] Make coqchk slightly happier with prelude/pretty

Unfortunately, it still fails in iris.prelude.pretty.pretty_N_inj
---
 theories/pretty.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/pretty.v b/theories/pretty.v
index 9f33bd6e..b72cb460 100644
--- a/theories/pretty.v
+++ b/theories/pretty.v
@@ -32,7 +32,8 @@ Lemma pretty_N_go_step x s :
   = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
 Proof.
   unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
-  unfold pretty_N_go_help; fold pretty_N_go_help.
+  destruct wf_guard. (* this makes coqchk happy. *)
+  unfold pretty_N_go_help at 1; fold pretty_N_go_help.
   by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
 Qed.
 Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.
-- 
GitLab