diff options
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/Setoid_ring_theory.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v index 021e2d1414..8b9ae52f0f 100644 --- a/contrib/ring/Setoid_ring_theory.v +++ b/contrib/ring/Setoid_ring_theory.v @@ -18,8 +18,7 @@ Section Setoid_rings. Variable A : Type. Variable Aequiv : A -> A -> Prop. -Infix "==" Aequiv (at level 5) - V8only (at level 50). +Infix Local "==" Aequiv (at level 5, no associativity). Variable S : (Setoid_Theory A Aequiv). |