From b66ddea9b0304d390b56afadda80fa4d2f2184d6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 23 Apr 2019 14:12:04 +0200 Subject: Replace nat_of_Z with Z.to_nat Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly. --- common/Memdata.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index a9ed48b4..307a02db 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -50,7 +50,7 @@ Proof. Qed. Definition size_chunk_nat (chunk: memory_chunk) : nat := - nat_of_Z(size_chunk chunk). + Z.to_nat(size_chunk chunk). Lemma size_chunk_conv: forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk). -- cgit