diff options
Diffstat (limited to 'theories/MSets/MSetList.v')
| -rw-r--r-- | theories/MSets/MSetList.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index 48af7e6a..bcf68f1d 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) - (** * Finite sets library *) (** This file proposes an implementation of the non-dependant @@ -788,8 +786,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Definition eq := L.eq. Definition eq_equiv := L.eq_equiv. Definition lt l1 l2 := - exists l1', exists l2', Ok l1' /\ Ok l2' /\ - eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'. + exists l1' l2', Ok l1' /\ Ok l2' /\ eq l1 l1' /\ eq l2 l2' /\ L.lt l1' l2'. Instance lt_strorder : StrictOrder lt. Proof. |