6 files changed, 19 insertions, 2 deletions
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index bc821532fe..bb873588b1 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -177,6 +177,7 @@ Section Defs.
    a rewrite crelation. *)
     
   Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+  Defined.
 
   (** Leibniz equality. *)
   Section Leibniz.
@@ -195,7 +196,10 @@ End Defs.
 
 (** Default rewrite crelations handled by [setoid_rewrite]. *)
 Instance: RewriteRelation impl.
+Defined.
+
 Instance: RewriteRelation iff.
+Defined.
 
 (** Hints to drive the typeclass resolution avoiding loops
  due to the use of full unification. *)
@@ -299,7 +303,8 @@ Section Binary.
     fun R R' => forall x y, iffT (R x y) (R' x y).
 
   Global Instance: RewriteRelation relation_equivalence.
-  
+  Defined.
+
   Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
     fun x y => prod (R x y) (R' x y).
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 4b97d75cea..6e2ff49536 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -171,6 +171,7 @@ Section Defs.
    a rewrite relation. *)
     
   Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA.
+  Defined.
 
   (** Leibniz equality. *)
   Section Leibniz.
@@ -189,7 +190,9 @@ End Defs.
 
 (** Default rewrite relations handled by [setoid_rewrite]. *)
 Instance: RewriteRelation impl.
+Defined.
 Instance: RewriteRelation iff.
+Defined.
 
 (** Hints to drive the typeclass resolution avoiding loops
  due to the use of full unification. *)
@@ -430,6 +433,7 @@ Section Binary.
     @predicate_equivalence (_::_::Tnil).
 
   Global Instance: RewriteRelation relation_equivalence.
+  Defined.
   
   Definition relation_conjunction (R : relation A) (R' : relation A) : relation A :=
     @predicate_intersection (A::A::Tnil) R R'.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 3e6358c8f3..341dacd4b2 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -62,7 +62,10 @@ Class Measure {A B} (f : A -> B).
 (** Standard measures. *)
 
 Instance fst_measure : @Measure (A * B) A Fst.
+Defined.
+
 Instance snd_measure : @Measure (A * B) B Snd.
+Defined.
 
 (** We define a product relation over [A*B]: each components should
     satisfy the corresponding initial relation. *)
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 3fab3c5a07..94920f74ec 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -41,6 +41,7 @@ Definition default_relation `{DefaultRelation A R} := R.
   (lowest priority). *)
 
 Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4.
+Defined.
 
 (** The setoid_replace tactics in Ltac, defined in terms of default relations
   and the setoid_rewrite tactic. *)
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 537400fb05..3d4b3d0568 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -40,7 +40,7 @@ Notation zero := (D0 Nil).
 
 (** For signed integers, we use two constructors [Pos] and [Neg]. *)
 
-Inductive int := Pos (d:uint) | Neg (d:uint).
+Variant int := Pos (d:uint) | Neg (d:uint).
 
 Declare Scope dec_uint_scope.
 Delimit Scope dec_uint_scope with uint.
@@ -50,6 +50,9 @@ Declare Scope dec_int_scope.
 Delimit Scope dec_int_scope with int.
 Bind Scope dec_int_scope with int.
 
+Register uint as num.uint.type.
+Register int as num.int.type.
+
 (** This representation favors simplicity over canonicity.
     For normalizing numbers, we need to remove head zero digits,
     and choose our canonical representation of 0 (here [D0 Nil]
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index ef2c688759..247827597a 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -29,6 +29,7 @@ Bind Scope positive_scope with positive.
 Arguments xO _%positive.
 Arguments xI _%positive.
 
+Register positive as num.pos.type.
 Register xI as num.pos.xI.
 Register xO as num.pos.xO.
 Register xH as num.pos.xH.