diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 08:54:45 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-09 08:54:45 +0000 |
| commit | 48fbc485c09e8a1657072cf87cd40ed9fd96ea43 (patch) | |
| tree | 8b737c8c928c7b54ffadcdc15205067d77050a66 /theories/Classes/Morphisms_Relations.v | |
| parent | 9471436ef062073bd12e25316f37921856a1fe6e (diff) | |
Fix compilation problem
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10768 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Morphisms_Relations.v')
| -rw-r--r-- | theories/Classes/Morphisms_Relations.v | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 284810e94..274389496 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -13,6 +13,9 @@ Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud 91405 Orsay, France *) +Require Import Coq.Classes.Morphisms. +Require Import Coq.Program.Program. + (** Morphisms for relations *) Instance relation_conjunction_morphism : Morphism (relation_equivalence (A:=A) ==> @@ -40,8 +43,8 @@ Proof. do 2 red. unfold predicate_implication. auto. Qed. Instance relation_equivalence_pointwise : Morphism (relation_equivalence ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) iff)) id. -Proof. apply (predicate_equivalence_pointwise (l:=(cons A (cons A nil)))). Qed. +Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed. Instance subrelation_pointwise : Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id. -Proof. apply (predicate_implication_pointwise (l:=(cons A (cons A nil)))). Qed. +Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed. |