From 83435e2c02cfe450eddde50eb92ed2b501f25dfc Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Thu, 29 Sep 2016 14:34:38 +0200 Subject: Ncring_initial: avoid a notation overriding --- plugins/setoid_ring/Ncring_initial.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring/Ncring_initial.v') diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 96885d2f7..20022c00e 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -18,7 +18,6 @@ Require Import BinInt. Require Import Setoid. Require Export Ncring. Require Export Ncring_polynom. -Import List. Set Implicit Arguments. @@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Notation "[ x ]" := (gen_phiZ x). + Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Local Open Scope ZMORPHISM. Definition get_signZ z := match z with -- cgit v1.2.3