From 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 17 Sep 2009 15:58:14 +0000 Subject: Delete trailing whitespaces in all *.{v,ml*} files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 9eef2bc1d..c5530e7ca 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -29,35 +29,35 @@ Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y - unfold Setoid_Theory. 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. - + -- cgit v1.2.3