Skip to content
Snippets Groups Projects
Commit c70cec15 authored by Hugo Herbelin's avatar Hugo Herbelin Committed by Robbert Krebbers
Browse files

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.
parent b4688b8a
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment