Rename obligations_tactic to obligation_tactic and fix bugs #1893.

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

1 files changed, 3 insertions, 3 deletions

diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index d96a532c3..b530cc098 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -40,7 +40,7 @@ Class [ equiv : Equivalence A ] => EqDec :=
 (** We define the [==] overloaded notation for deciding equality. It does not take precedence
    of [==] defined in the type scope, hence we can have both at the same time. *)
 
-Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70).
+Notation " x == y " := (equiv_dec (x :>) (y :>)) (no associativity, at level 70) : equiv_scope.
 
 Definition swap_sumbool {A B} (x : { A } + { B }) : { B } + { A } :=
   match x with
@@ -58,7 +58,7 @@ Program Definition nequiv_dec [ EqDec A ] (x y : A) : { x =/= y } + { x === y }
 
 (** Overloaded notation for inequality. *)
 
-Infix "=/=" := nequiv_dec (no associativity, at level 70).
+Infix "<>" := nequiv_dec (no associativity, at level 70) : equiv_scope.
 
 (** Define boolean versions, losing the logical information. *)
 
@@ -155,4 +155,4 @@ Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq :=
   Next Obligation.
   Proof. clear aux. red in H0. subst. 
     destruct y; intuition (discriminate || eauto).
-  Defined.
\ No newline at end of file
+  Defined.