Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 9 insertions, 9 deletions

diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index a1a78acc..29494069 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -5,19 +5,19 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+(* $Id: Basics.v 11709 2008-12-20 11:42:15Z msozeau $ *)
 
-(* Standard functions and combinators.
- * Proofs about them require functional extensionality and can be found in [Combinators].
- *
- * Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
- *              91405 Orsay, France *)
+(** Standard functions and combinators.
+   
+   Proofs about them require functional extensionality and can be found in [Combinators].
 
-(* $Id: Basics.v 11046 2008-06-03 22:48:06Z msozeau $ *)
+   Author: Matthieu Sozeau
+   Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+   91405 Orsay, France *)
 
-(** The polymorphic identity function. *)
+(** The polymorphic identity function is defined in [Datatypes]. *)
 
-Definition id {A} := fun x : A => x.
+Implicit Arguments id [[A]].
 
 (** Function composition. *)