From 73c48fb2aa95502a7431a7f766c134ee6c7278b1 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 21 Feb 2023 16:53:16 +0000
Subject: [PATCH] adapt for coq/coq#17133
---
theories/Data/HList.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/Data/HList.v b/theories/Data/HList.v
index f6e49971..0c15cb79 100644
--- a/theories/Data/HList.v
+++ b/theories/Data/HList.v
@@ -678,7 +678,7 @@ Section hlist.
(projT2 x) (hlist_app vs vs') = y vs'.
Proof.
clear. induction tvs; simpl; intros.
- { rewrite <- Minus.minus_n_O.
+ { rewrite PeanoNat.Nat.sub_0_r.
rewrite H0. destruct x. simpl.
eexists; split; eauto. intros.
rewrite (hlist_eta vs). reflexivity. }