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

6 files changed, 16 insertions, 13 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.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 0d464b84e..05167bdc5 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
+(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.Morphisms"); compile-command: "make -C ../.. TIME='time'" -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -434,6 +434,7 @@ Qed.
 Lemma morphism_releq_morphism [ Normalizes A R R', Morphism _ R' m ] : Morphism R m.
 Proof.
   intros.
+
   pose respect as r.
   pose normalizes as norm.
   setoid_rewrite norm.
@@ -464,4 +465,4 @@ Ltac morphism_reflexive :=
     | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism
   end.
 
-Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
\ No newline at end of file
+Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 044195f19..31398aa3b 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
+(* -*- coq-prog-name: "coqtop.byte"; coq-prog-args: ("-emacs-U" "-top" "Coq.Classes.RelationClasses") -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -91,7 +91,7 @@ Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A)
     unfold complement.
     red. intros H.
     intros H' ; apply H'.
-    apply (reflexivity H).
+    apply reflexivity.
   Qed.
 
 
@@ -129,7 +129,7 @@ Ltac simpl_relation :=
   unfold flip, impl, arrow ; try reduce ; program_simpl ;
     try ( solve [ intuition ]).
 
-Ltac obligations_tactic ::= simpl_relation.
+Ltac obligation_tactic ::= simpl_relation.
 
 (** Logical implication. *)
 
@@ -171,7 +171,7 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop :=
 
 (** An Equivalence is a PER plus reflexivity. *)
 
-Instance Equivalence_PER [ Equivalence A R ] : PER A R :=
+Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
   PER_Symmetric := Equivalence_Symmetric ;
   PER_Transitive := Equivalence_Transitive.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index c5a8f3d30..227a93207 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -142,7 +142,7 @@ Program Instance type_equivalence : Equivalence Type type_eq.
 
 Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
 
-Ltac obligations_tactic ::= morphism_tac.
+Ltac obligation_tactic ::= morphism_tac.
 
 (** These are morphisms used to rewrite at the top level of a proof, 
    using [iff_impl_id_morphism] if the proof is in [Prop] and
@@ -178,4 +178,4 @@ Infix "=~=" := pequiv (at level 70, no associativity) : type_scope.
 
 (** Reset the default Program tactic. *)
 
-Ltac obligations_tactic ::= program_simpl.
+Ltac obligation_tactic ::= program_simpl.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index aea6f5d7a..ff5f7cb6c 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -174,3 +174,5 @@ Ltac default_add_morphism_tactic :=
   end.
 
 Ltac add_morphism_tactic := default_add_morphism_tactic.
+
+Ltac obligation_tactic ::= program_simpl.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 5182123f4..45e965142 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -222,7 +222,7 @@ Ltac refine_hyp c :=
     end.
 
 (** The default simplification tactic used by Program is defined by [program_simpl], sometimes [auto]
-   is not enough, better rebind using [Obligations Tactic := tac] in this case, 
+   is not enough, better rebind using [Obligation Tactic := tac] in this case, 
    possibly using [program_simplify] to use standard goal-cleaning tactics. *)
 
 Ltac program_simplify :=
@@ -231,4 +231,4 @@ Ltac program_simplify :=
 
 Ltac program_simpl := program_simplify ; auto.
 
-Ltac obligations_tactic := program_simpl.
+Ltac obligation_tactic := program_simpl.