From c2e3d63ca60b27abb5398ecbc8ebcaf8fb925206 Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 18 Jan 2008 19:41:43 +0000 Subject: 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 --- theories/Classes/SetoidClass.v | 30 +++++++++++++++++------------- 1 file changed, 17 insertions(+), 13 deletions(-) (limited to 'theories/Classes/SetoidClass.v') 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. -- cgit v1.2.3