diff options
Diffstat (limited to 'plugins/ring')
| -rw-r--r-- | plugins/ring/LegacyArithRing.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index fd5bcd9355..94dc48a733 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -13,7 +13,7 @@ Require Export LegacyRing. Require Export Arith. Require Import Eqdep_dec. -Open Local Scope nat_scope. +Local Open Scope nat_scope. Fixpoint nateq (n m:nat) {struct m} : bool := match n, m with |