6 files changed, 3 insertions, 7 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 9259d490fb..fd5bcd9355 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -15,7 +15,7 @@ Require Import Eqdep_dec.
 
 Open Local Scope nat_scope.
 
-Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
+Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
   | O, O => true
   | S n', S m' => nateq n' m'
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index fa77099826..5dcd6d840d 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
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 87b64c8d8f..5845062dd2 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 Require Import Eqdep_dec.
 Require Import LegacyRing.
 
-Unboxed Definition Zeq (x y:Z) :=
+Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
   | Datatypes.Eq => true
   | _ => false
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index e009f14eaa..1763d70a62 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -10,8 +10,6 @@ Require Import LegacyRing_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
-Unset Boxed Definitions.
-
 Section abstract_semi_rings.
 
 Inductive aspolynomial : Type :=
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index 073cd2f63c..e499f22201 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -10,7 +10,6 @@ Require Import LegacyRing_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index d157bffce9..41190e8d9a 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -10,7 +10,6 @@ Require Import Setoid_ring_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.