Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a wrapper around Ltac program_simpl ::= .

!!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules.



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

1 files changed, 17 insertions, 13 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index adfd1c3a3..3043a9239 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -166,25 +166,25 @@ Class [ sa : Setoid a eqa, sb : Setoid b eqb ] => Morphism (m : a -> b) :=
 
 Definition respecting [ Setoid a R, Setoid b R' ] : Type := { morph : a -> b | respectful morph }.
 
-Obligations Tactic := try red ; program_simpl ; unfold equiv in * ; try tauto.
+Ltac program_simpl ::= try red ; default_program_simpl ; try tauto.
 
 Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid : 
   Setoid ({ morph : a -> b | respectful morph })
   (fun (f g : respecting) => forall (x y : a), R x y -> R' (`f x) (`g y)) :=
   equiv_prf := Build_equivalence _ _ _ _ _.
 
-Next Obligation.
-Proof.
-  trans (y x0) ; eauto.
-  apply H.
-  refl.
-Qed.
+  Next Obligation.
+  Proof.
+    trans (y x0) ; eauto.
+    apply H.
+    refl.
+  Qed.
 
-Next Obligation.
-Proof.
-  sym ; apply H.
-  sym ; auto.
-Qed.
+  Next Obligation.
+  Proof.
+    sym ; apply H.
+    sym ; auto.
+  Qed.
 
 (** We redefine respect for binary and ternary morphims because we cannot get a satisfying instance of [Setoid (a -> b)] from 
    some arbitrary domain and codomain setoids. We can define it on respectful Coq functions though, see [arrow_setoid] above. *)
@@ -321,4 +321,8 @@ Program Instance [ sa : Setoid a R, sb : Setoid b R' ] => arrow_setoid :
   Setoid (a -> b)
   (fun f g => forall (x y : a), R x y -> R' (f x) (g y)) :=
   equiv_prf := Build_equivalence _ _ _ _ _.
-*)
\ No newline at end of file
+*)
+
+(** Reset the default Program tactic. *)
+
+Ltac program_simpl ::= default_program_simpl.