From c70cec15c5f1651262221e83a04c96f2a5168640 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <hugo.herbelin@inria.fr>
Date: Wed, 2 Sep 2020 19:43:48 +0200
Subject: [PATCH] Swap import of Peano and Utf8 to ensure that Utf8 notations
 are preferred.

This is a consequence of Coq PR #12950 which gives to import the
effect of reactivating the imported notations.
---
 theories/base.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index c0ff4f96..6513ea41 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -6,7 +6,9 @@ structures. *)
 (* We want to ensure that [le] and [lt] refer to operations on [nat].
 These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
 we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Peano.
+(* We also want to ensure that notations from [Coq.Utf8] take precedence
+over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
+From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
 Set Default Proof Using "Type".
 Export ListNotations.
-- 
GitLab