From ef839489f85f0d8657101eccecf60a472672edd9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 May 2020 09:31:23 +0200
Subject: [PATCH] Alternative take on #153: import `Arith` in `base`.

Also use `Arith` instead of `NPeano`, since the latter is deprecated.
---
 theories/base.v    | 2 +-
 theories/numbers.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 7d63f124..a4cfdfb3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -3,7 +3,7 @@ that are used throughout the whole development. Most importantly it contains
 abstract interfaces for ordered structures, sets, and various other data
 structures. *)
 
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid.
+From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Arith.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
diff --git a/theories/numbers.v b/theories/numbers.v
index d0b9d29d..663fde2a 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1,7 +1,7 @@
 (** This file collects some trivial facts on the Coq types [nat] and [N] for
 natural numbers, and the type [Z] for integers. It also declares some useful
 notations. *)
-From Coq Require Export EqdepFacts PArith NArith ZArith NPeano.
+From Coq Require Export EqdepFacts PArith NArith ZArith.
 From Coq Require Import QArith Qcanon.
 From stdpp Require Export base decidable option.
 Set Default Proof Using "Type".
-- 
GitLab