diff options
Diffstat (limited to 'theories/FSets/FSetToFiniteSet.v')
| -rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 23420109c..01138270e 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* Finite sets library. - * Authors: Pierre Letouzey and Jean-Christophe Filliâtre - * Institution: LRI, CNRS UMR 8623 - Université Paris Sud - * 91405 Orsay, France *) - (* $Id$ *) +(** * Finite sets library : conversion to old [Finite_sets] *) + Require Import Ensembles Finite_sets. Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx. |