diff options
Diffstat (limited to 'theories/Setoids/Setoid.v')
| -rw-r--r-- | theories/Setoids/Setoid.v | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index a187a7c6..db4d699f 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -6,11 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Setoid.v 12187 2009-06-13 19:36:59Z msozeau $: i*) +(*i $Id$: i*) Require Export Coq.Classes.SetoidTactics. -Export Morphisms.MorphismNotations. +Export Morphisms.ProperNotations. (** For backward compatibility *) @@ -18,46 +18,46 @@ Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. - unfold Setoid_Theory. intros ; reflexivity. + unfold Setoid_Theory in s. intros ; reflexivity. Defined. Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. - unfold Setoid_Theory. intros ; symmetry ; assumption. + unfold Setoid_Theory in s. intros ; symmetry ; assumption. Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. - unfold Setoid_Theory. intros ; transitivity y ; assumption. + unfold Setoid_Theory in s. intros ; transitivity y ; assumption. Defined. -(** Some tactics for manipulating Setoid Theory not officially +(** Some tactics for manipulating Setoid Theory not officially declared as Setoid. *) Ltac trans_st x := idtac "trans_st on Setoid_Theory is OBSOLETE"; idtac "use transitivity on Equivalence instead"; match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => apply (Seq_trans _ _ H) with x; auto end. Ltac sym_st := idtac "sym_st on Setoid_Theory is OBSOLETE"; idtac "use symmetry on Equivalence instead"; - match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + match goal with + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => apply (Seq_sym _ _ H); auto end. Ltac refl_st := idtac "refl_st on Setoid_Theory is OBSOLETE"; idtac "use reflexivity on Equivalence instead"; - match goal with - | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => + match goal with + | H : Setoid_Theory _ ?eqA |- ?eqA _ _ => apply (Seq_refl _ _ H); auto end. Definition gen_st : forall A : Set, Setoid_Theory _ (@eq A). -Proof. - constructor; congruence. +Proof. + constructor; congruence. Qed. - + |