7 files changed, 13 insertions, 8 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 4f7fdb34c..0d42dabfd 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -16,7 +16,7 @@ Require Import Eqdep_dec.
 
 Open Local Scope nat_scope.
 
-Fixpoint nateq (n m:nat) {struct m} : bool :=
+Unboxed 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/contrib/ring/NArithRing.v b/contrib/ring/NArithRing.v
index ebc6a69ca..41e3a7d7b 100644
--- a/contrib/ring/NArithRing.v
+++ b/contrib/ring/NArithRing.v
@@ -15,7 +15,7 @@ Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
 
-Definition Neq (n m:N) :=
+Unboxed Definition Neq (n m:N) :=
   match (n ?= m)%N with
   | Datatypes.Eq => true
   | _ => false
@@ -41,4 +41,4 @@ Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
     apply Neq_prop.
 Qed.
 
-Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
-\ No newline at end of file
+Add Semi Ring N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index b89a850bf..9a11a70b9 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -26,6 +26,7 @@
 ***********************************************************************)
 
 Set Implicit Arguments.
+Unset Boxed Definitions.
 
 Section variables_map.
 
@@ -81,4 +82,4 @@ Qed.
 
 End variables_map.
 
-Unset Implicit Arguments.
-\ No newline at end of file
+Unset Implicit Arguments.
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index ef58f51c9..5d5046393 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -12,6 +12,8 @@ Require Import Ring_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
+Unset Boxed Definitions.
+
 Section abstract_semi_rings.
 
 Inductive aspolynomial : Type :=
@@ -701,4 +703,4 @@ Proof.
     rewrite H; reflexivity.
 Qed.  
 
-End abstract_rings.
-\ No newline at end of file
+End abstract_rings.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index fb194e52a..bd22fa39a 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -12,6 +12,7 @@ Require Import 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.
@@ -898,4 +899,4 @@ Infix "*" := Pmult : ring_scope.
 Notation "- x" := (Popp x) : ring_scope.
 Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
 
-Delimit Scope ring_scope with ring.
-\ No newline at end of file
+Delimit Scope ring_scope with ring.
diff --git a/contrib/ring/Setoid_ring_normalize.v b/contrib/ring/Setoid_ring_normalize.v
index 2a2ec3720..aa6d95eab 100644
--- a/contrib/ring/Setoid_ring_normalize.v
+++ b/contrib/ring/Setoid_ring_normalize.v
@@ -12,7 +12,8 @@ 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.
   simple induction n; simple induction m; simpl in |- *;
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index c726f7eea..9324fb602 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -14,7 +14,7 @@ Require Export ArithRing.
 Require Export ZArith_base.
 Require Import Eqdep_dec.
 
-Definition Zeq (x y:Z) :=
+Unboxed Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
   | Datatypes.Eq => true
   | _ => false