diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-14 10:11:18 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-08-14 10:11:18 +0000 |
| commit | 1dc7de4956abd629f506e605924c645c6fd5e224 (patch) | |
| tree | 9aac2d9c10420834969b0cdeffc1a0e2e2688845 /theories/FSets | |
| parent | 6fd0922df95052a7adf68c0fc131bf32365386fb (diff) | |
comparison functions should be Defined not Qed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9066 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 012b6bfb3..b3227e5a8 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -66,7 +66,7 @@ Module Nat_as_OT <: UsualOrderedType. constructor 1; auto. constructor 2; auto. intro; constructor 3; auto. - Qed. + Defined. End Nat_as_OT. @@ -182,7 +182,7 @@ Module N_as_OT <: UsualOrderedType. destruct (Nle x y); auto. destruct (x ?= y)%N; simpl; try discriminate. intros (H0,_); elim H0; auto. - Qed. + Defined. End N_as_OT. @@ -242,7 +242,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. apply EQ; unfold eq; auto. apply GT; unfold lt; auto. apply GT; unfold lt; auto. - Qed. + Defined. End PairOrderedType. |