From 1dc7de4956abd629f506e605924c645c6fd5e224 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 14 Aug 2006 10:11:18 +0000 Subject: 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 --- theories/FSets/OrderedTypeEx.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/FSets') 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. -- cgit v1.2.3