diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 4f24263373..bb3cfc5a8a 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.v @@ -897,6 +897,6 @@ End rings. Infix "+" := Pplus : ring_scope. Infix "*" := Pmult : ring_scope. Notation "- x" := (Popp x) : ring_scope. -Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope. +Notation "[ x ]" := (Pvar x) : ring_scope. Delimit Scope ring_scope with ring. |