diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 18:19:32 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-13 18:19:32 +0000 |
| commit | 577d275822c7a266f865952bdcf2dd41861b5b21 (patch) | |
| tree | be2d4c0e6a05ef8f43605cba4a4bcb02259ec0c6 /theories/Classes | |
| parent | bc50989dea9a5bd1b4ec891e63d67fd3fd2f9c3e (diff) | |
Debugging of the class_setoid tactic and eauto. Prepare for move from
class_setoid to class_tactics...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10563 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Relations.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/theories/Classes/Relations.v b/theories/Classes/Relations.v index 9cc78a970..c05a4b1e1 100644 --- a/theories/Classes/Relations.v +++ b/theories/Classes/Relations.v @@ -184,6 +184,12 @@ Ltac relation_refl := | [ |- ?R ?A ?B ?C ?D ?X ?X ] => apply (reflexive (R:=R A B C D) X) | [ H : ?R ?A ?B ?C ?D ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D) H) + + | [ |- ?R ?A ?B ?C ?D ?E ?X ?X ] => apply (reflexive (R:=R A B C D E) X) + | [ H : ?R ?A ?B ?C ?D ?E ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E) H) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?X ] => apply (reflexive (R:=R A B C D E F) X) + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?X |- _ ] => apply (irreflexive (R:=R A B C D E F) H) end. Ltac refl := relation_refl. @@ -200,6 +206,9 @@ Ltac relation_sym := | [ H : ?R ?A ?B ?C ?D ?X ?Y |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y) H) + | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y) H) + + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y) H) end. Ltac relation_symmetric := @@ -213,6 +222,10 @@ Ltac relation_symmetric := | [ |- ?R ?A ?B ?C ?Y ?X ] => apply (symmetric (R:=R A B C) (x:=X) (y:=Y)) | [ |- ?R ?A ?B ?C ?D ?Y ?X ] => apply (symmetric (R:=R A B C D) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?D ?E ?Y ?X ] => apply (symmetric (R:=R A B C D E) (x:=X) (y:=Y)) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?Y ?X ] => apply (symmetric (R:=R A B C D E F) (x:=X) (y:=Y)) end. Ltac sym := relation_symmetric. @@ -236,6 +249,9 @@ Ltac relation_trans := | [ H : ?R ?A ?B ?C ?D ?E ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z) H H') + + | [ H : ?R ?A ?B ?C ?D ?E ?F ?X ?Y, H' : ?R ?A ?B ?C ?D ?E ?F ?Y ?Z |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => + apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z) H H') end. Ltac relation_transitive Y := @@ -254,6 +270,12 @@ Ltac relation_transitive Y := | [ |- ?R ?A ?B ?C ?D ?X ?Z ] => apply (transitive (R:=R A B C D) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?E ?X ?Z ] => + apply (transitive (R:=R A B C D E) (x:=X) (y:=Y) (z:=Z)) + + | [ |- ?R ?A ?B ?C ?D ?E ?F ?X ?Z ] => + apply (transitive (R:=R A B C D E F) (x:=X) (y:=Y) (z:=Z)) end. Ltac trans Y := relation_transitive Y. |