diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /theories/FSets/OrderedTypeEx.v | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'theories/FSets/OrderedTypeEx.v')
-rw-r--r-- | theories/FSets/OrderedTypeEx.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 1c5a4054..6fa6a85c 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -11,7 +11,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrderedTypeEx.v 8836 2006-05-20 21:34:27Z letouzey $ *) +(* $Id: OrderedTypeEx.v 9066 2006-08-14 10:11:18Z letouzey $ *) Require Import OrderedType. Require Import ZArith. @@ -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. |