diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-18 11:22:13 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-18 11:22:13 +0000 |
| commit | d4685a5bdaf15c31ddc616777b05280ec7570d08 (patch) | |
| tree | 1349f628eb8cb3dcfbaf9d5d78bce185f10a8f39 /theories/Classes/Equivalence.v | |
| parent | 99541c1123793d1c6352d1326c40426024b55948 (diff) | |
Correct implementation of normalization of signatures using setoid
rewriting, in some sense bootstrapping the system. Remove redundant
morphisms for now to test for completeness (small performance penalty).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10689 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Equivalence.v')
| -rw-r--r-- | theories/Classes/Equivalence.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index b90fdc97e..5543f615d 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -26,6 +26,11 @@ Require Export Coq.Classes.SetoidTactics. Set Implicit Arguments. Unset Strict Implicit. +(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) + +Instance [ ! Equivalence A R ] => + equivalence_default : DefaultRelation A R | 4. + Definition equiv [ Equivalence A R ] : relation A := R. (** Shortcuts to make proof search possible (unification won't unfold equiv). *) @@ -152,8 +157,3 @@ Notation " x =~= y " := (pequiv x y) (at level 70, no associativity) : type_scop (** Reset the default Program tactic. *) Ltac obligations_tactic ::= program_simpl. - -(** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) - -Instance [ ! Equivalence A R ] => - equivalence_default : DefaultRelation A R | 4. |