diff options
Diffstat (limited to 'theories/Classes/RelationPairs.v')
| -rw-r--r-- | theories/Classes/RelationPairs.v | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index 7972c96c..2b010206 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -15,27 +15,25 @@ Require Import Relations Morphisms. fix the simpl tactic, since "simpl fst" would be refused for the moment. -Implicit Arguments fst [[A] [B]]. -Implicit Arguments snd [[A] [B]]. -Implicit Arguments pair [[A] [B]]. +Arguments fst {A B}. +Arguments snd {A B}. +Arguments pair {A B}. /NB *) Local Notation Fst := (@fst _ _). Local Notation Snd := (@snd _ _). -Arguments Scope relation_conjunction - [type_scope signature_scope signature_scope]. -Arguments Scope relation_equivalence - [type_scope signature_scope signature_scope]. -Arguments Scope subrelation [type_scope signature_scope signature_scope]. -Arguments Scope Reflexive [type_scope signature_scope]. -Arguments Scope Irreflexive [type_scope signature_scope]. -Arguments Scope Symmetric [type_scope signature_scope]. -Arguments Scope Transitive [type_scope signature_scope]. -Arguments Scope PER [type_scope signature_scope]. -Arguments Scope Equivalence [type_scope signature_scope]. -Arguments Scope StrictOrder [type_scope signature_scope]. +Arguments relation_conjunction A%type (R R')%signature _ _. +Arguments relation_equivalence A%type (_ _)%signature. +Arguments subrelation A%type (R R')%signature. +Arguments Reflexive A%type R%signature. +Arguments Irreflexive A%type R%signature. +Arguments Symmetric A%type R%signature. +Arguments Transitive A%type R%signature. +Arguments PER A%type R%signature. +Arguments Equivalence A%type R%signature. +Arguments StrictOrder A%type R%signature. Generalizable Variables A B RA RB Ri Ro f. @@ -88,10 +86,10 @@ Section RelCompFun_Instances. `(Measure A B f, Irreflexive _ R) : Irreflexive (R@@f). Proof. firstorder. Qed. - Global Instance RelCompFun_Equivalence + Global Program Instance RelCompFun_Equivalence `(Measure A B f, Equivalence _ R) : Equivalence (R@@f). - Global Instance RelCompFun_StrictOrder + Global Program Instance RelCompFun_StrictOrder `(Measure A B f, StrictOrder _ R) : StrictOrder (R@@f). End RelCompFun_Instances. @@ -108,7 +106,7 @@ Instance RelProd_Transitive {A B}(RA:relation A)(RB:relation B) `(Transitive _ RA, Transitive _ RB) : Transitive (RA*RB). Proof. firstorder. Qed. -Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) +Program Instance RelProd_Equivalence {A B}(RA:relation A)(RB:relation B) `(Equivalence _ RA, Equivalence _ RB) : Equivalence (RA*RB). Lemma FstRel_ProdRel {A B}(RA:relation A) : |