diff options
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index a9bdaa8f..178d5333 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) -(* $Id: SetoidClass.v 11065 2008-06-06 22:39:43Z msozeau $ *) +(* $Id: SetoidClass.v 11282 2008-07-28 11:51:53Z msozeau $ *) Set Implicit Arguments. Unset Strict Implicit. @@ -41,13 +41,13 @@ Typeclasses unfold equiv. (** Shortcuts to make proof search easier. *) Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Existing Instance setoid_refl. Existing Instance setoid_sym. @@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv := - trans_sym_morphism. + PER_morphism. (** Add this very useful instance in the database. *) @@ -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. |