aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/omega/Zlogarithm.v
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/omega/Zlogarithm.v')
-rw-r--r--contrib/omega/Zlogarithm.v16
1 files changed, 2 insertions, 14 deletions
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
index 87f1f87c5..c5b36397f 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/contrib/omega/Zlogarithm.v
@@ -1,17 +1,5 @@
-(****************************************************************************)
-(* The Calculus of Inductive Constructions *)
-(* *)
-(* Projet Coq *)
-(* *)
-(* INRIA LRI-CNRS ENS-CNRS *)
-(* Rocquencourt Orsay Lyon *)
-(* *)
-(* Coq V6.3 *)
-(* July 1st 1999 *)
-(* *)
-(****************************************************************************)
-(* Zlogarithm.v *)
-(****************************************************************************)
+
+(* $Id$ *)
(****************************************************************************)
(* The integer logarithms with base 2. There are three logarithms, *)