Support "Local Obligation Tactic" (now the default in sections).

Update Numbers that was implicitely using [simpl_relation] instead of
the default tactic [program_simpl].


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12647 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 3 insertions, 0 deletions

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.