diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-17 17:16:03 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-01-17 17:16:03 +0000 |
| commit | edbb81e324234548c2bb70306fb448420e1bbd70 (patch) | |
| tree | 2711b59c9c2fe9a9df0b8c716af33a0108cfc8e1 /theories/Classes/SetoidTactics.v | |
| parent | cd21f033922b22f855111e171ece9591009cf15b (diff) | |
Fix Makefile bug, using .v instead of .vo and document SetoidDec.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10447 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidTactics.v')
| -rw-r--r-- | theories/Classes/SetoidTactics.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 65b2968cc..540ac184e 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -7,7 +7,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Certified Haskell Prelude. +(* Tactics for typeclass-based setoids. + * * Author: Matthieu Sozeau * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) @@ -21,7 +22,8 @@ Unset Strict Implicit. Require Export Coq.Classes.SetoidClass. -Ltac rew H := clrewrite H. +(* Application of the extensionality axiom to turn a goal on leibinz equality to + a setoid equivalence. *) Lemma setoideq_eq [ sa : Setoid a eqa ] : forall x y, eqa x y -> x = y. Proof. @@ -31,6 +33,7 @@ Qed. Implicit Arguments setoideq_eq [[a] [eqa] [sa]]. (** Application of the extensionality principle for setoids. *) + Ltac setoideq_ext := match goal with [ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) X Y) |