diff options
Diffstat (limited to 'plugins/ring/LegacyNArithRing.v')
| -rw-r--r-- | plugins/ring/LegacyNArithRing.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index fa7709982..5dcd6d840 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -14,7 +14,7 @@ Require Export ZArith_base. Require Import NArith. Require Import Eqdep_dec. -Unboxed Definition Neq (n m:N) := +Definition Neq (n m:N) := match (n ?= m)%N with | Datatypes.Eq => true | _ => false |