diff options
| author | Hugo Herbelin | 2018-03-30 14:47:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-10 13:07:29 +0200 |
| commit | 46ab3659dd1f2e4839064cfabc03bd19268fa44b (patch) | |
| tree | a4b215eb3289a189c9756bf44c3e52d04f306c99 /theories/Numbers/Integer/NatPairs | |
| parent | 8e675d70ad1f60cbbf9f1e630ce6dee61347c7ca (diff) | |
Adapting standard library to the introduction of "Declare Scope".
Removing in passing two Local which are no-ops in practice.
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. |