Merge pull request #747 from proux01/coq_18164

Adapt to coq/coq#18164
PrincetonUniversity · Nov 27, 2023 · 6d2eb96 · 6d2eb96
2 parents 8633963 + c1e7f88
commit 6d2eb96
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/floyd/reptype_lemmas.v b/floyd/reptype_lemmas.v
@@ -1183,7 +1183,7 @@ change 0 with (Z.of_nat 0).
 rewrite Zlength_correct.
 rewrite replist_firstn_skipn by lia.
 rewrite skipn_0 by auto.
-rewrite NPeano.Nat.sub_0_r.
+rewrite Nat.sub_0_r.
 apply firstn_exact_length.
 Qed.
 

diff --git a/msl/tree_shares.v b/msl/tree_shares.v
@@ -10,9 +10,7 @@ Require Import VST.msl.sepalg.
 Require Import VST.msl.boolean_alg.
 
 Require Import Recdef.
-Require Import NPeano.
 Require Import ZArith.
-Require Import Coq.Arith.Max.
 
 (** This module implements a share model
     via binary trees with boolean-labeled leaves.