diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-29 14:34:38 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-09-29 14:34:38 +0200 |
| commit | 83435e2c02cfe450eddde50eb92ed2b501f25dfc (patch) | |
| tree | 24e84c85f0342ebb0b5882a66401b22015ced80b /plugins/setoid_ring/Ncring_initial.v | |
| parent | af051436672561b4c15e07dfe4f9cee93f0741a4 (diff) | |
Ncring_initial: avoid a notation overriding
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 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 |