Skip to content
Snippets Groups Projects
Commit 897b954e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master+adapt-coq-pr12950-notation-registering-reworking' into 'master'

Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.

See merge request iris/stdpp!183
parents 7e802184 c70cec15
No related branches found
No related tags found
1 merge request!183Swap import of Peano and Utf8 to ensure that Utf8 notations are preferred.
Pipeline #33451 passed
...@@ -6,7 +6,9 @@ structures. *) ...@@ -6,7 +6,9 @@ structures. *)
(* We want to ensure that [le] and [lt] refer to operations on [nat]. (* 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], 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]. *) 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. From Coq Require Import Permutation.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Export ListNotations. 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