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 /plugins/setoid_ring/Ncring_initial.v | |
| 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 'plugins/setoid_ring/Ncring_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with |