aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-01 17:14:39 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-01 17:14:39 +0000
commitf0660f6a814a7f8728a6cbb9fdd11499a8dbdca2 (patch)
tree309c9a5669f957be8b2a4484f4579eb707408085 /theories/Relations
parentef0c1fc9594fd0e8711104274d358eb4f0bbf76d (diff)
Passage de 'relation' à Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4288 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Relations')
-rwxr-xr-xtheories/Relations/Relation_Definitions.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index 35c670574..32f433d07 100755
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -10,7 +10,7 @@
Section Relation_Definition.
- Variable A: Set.
+ Variable A: Type.
Definition relation := A -> A -> Prop.