diff options
Diffstat (limited to 'plugins/setoid_ring/Ncring_initial.v')
| -rw-r--r-- | plugins/setoid_ring/Ncring_initial.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 96885d2f..20022c00 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 |