diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Classes/RelationPairs.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
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) : |