9 files changed, 11 insertions, 3 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index cc8d79c03..d0f243474 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -26,6 +26,7 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 Generalizable Variables A R eqA B S eqB.
+Local Obligation Tactic := simpl_relation.
 
 Open Local Scope signature_scope.
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index dceb49cb6..2fd85ce2e 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -21,6 +21,7 @@ Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
 Generalizable All Variables.
+Local Obligation Tactic := simpl_relation.
 
 (** * Morphisms.
 
diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v
index dbe7b5c88..2dc033d24 100644
--- a/theories/Classes/Morphisms_Prop.v
+++ b/theories/Classes/Morphisms_Prop.v
@@ -16,7 +16,7 @@ Require Import Coq.Classes.Morphisms.
 Require Import Coq.Program.Basics.
 Require Import Coq.Program.Tactics.
 
-Obligation Tactic := simpl_relation.
+Local Obligation Tactic := simpl_relation.
 
 (** Standard instances for [not], [iff] and [impl]. *)
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 2caaa063a..9b8485519 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -134,7 +134,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Obligation Tactic := simpl_relation.
+Local Obligation Tactic := simpl_relation.
 
 (** Logical implication. *)
 
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 6a2745d34..cf3986b72 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -35,6 +35,7 @@ Qed.
 (** Basic operations. *)
 
 Instance eq_equiv : Equivalence (@eq Z).
+Local Obligation Tactic := simpl_relation.
 Program Instance succ_wd : Proper (eq==>eq) Zsucc.
 Program Instance pred_wd : Proper (eq==>eq) Zpred.
 Program Instance add_wd : Proper (eq==>eq==>eq) Zplus.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index e94644c48..93922aa43 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -32,6 +32,7 @@ Qed.
 (** Basic operations. *)
 
 Instance eq_equiv : Equivalence (@eq N).
+Local Obligation Tactic := simpl_relation.
 Program Instance succ_wd : Proper (eq==>eq) Nsucc.
 Program Instance pred_wd : Proper (eq==>eq) Npred.
 Program Instance add_wd : Proper (eq==>eq==>eq) Nplus.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 73affd90d..962bc8de0 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -28,6 +28,7 @@ Qed.
 (** Basic operations. *)
 
 Instance eq_equiv : Equivalence (@eq nat).
+Local Obligation Tactic := simpl_relation.
 Program Instance succ_wd : Proper (eq==>eq) S.
 Program Instance pred_wd : Proper (eq==>eq) pred.
 Program Instance add_wd : Proper (eq==>eq==>eq) plus.
@@ -228,6 +229,7 @@ Module NDivMod <: NDivSig.
  Definition modulo := modulo.
  Definition div_mod := div_mod.
  Definition mod_upper_bound := mod_upper_bound.
+ Local Obligation Tactic := simpl_relation.
  Program Instance div_wd : Proper (eq==>eq==>eq) div.
  Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 End NDivMod.
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index 59784553a..bea0429dd 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -9,7 +9,7 @@
 
 Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms.
 Require Export ZOdiv_def.
-Require Zdiv ZBinary ZDivTrunc.
+Require Zdiv Binary.ZBinary ZDivTrunc.
 
 Open Scope Z_scope.
 
@@ -249,6 +249,7 @@ Qed.
 Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod.
  Definition div := ZOdiv.
  Definition modulo := ZOmod.
+ Local Obligation Tactic := simpl_relation.
  Program Instance div_wd : Proper (eq==>eq==>eq) div.
  Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
 
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index a07b6d038..e9e963f97 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -306,6 +306,7 @@ Qed.
 Module ZDiv <: ZDivFloor.ZDiv ZBinary.ZBinAxiomsMod.
  Definition div := Zdiv.
  Definition modulo := Zmod.
+ Local Obligation Tactic := simpl_relation.
  Program Instance div_wd : Proper (eq==>eq==>eq) div.
  Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.