aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/Binary
diff options
context:
space:
mode:
authorletouzey2008-05-15 21:58:20 +0000
committerletouzey2008-05-15 21:58:20 +0000
commit972a60b36778a5c6971aa3f9a72073fd19f02b84 (patch)
tree1bba36e3cd3eb367c0f6d9535fa4b1eee871e66b /theories/Numbers/Natural/Binary
parent3d267e1a4c3b908beeae5907a00e6c9a9210117b (diff)
Coq headers + $ in theories/Numbers files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10934 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Binary')
-rw-r--r--theories/Numbers/Natural/Binary/NBinDefs.v2
-rw-r--r--theories/Numbers/Natural/Binary/NBinary.v12
2 files changed, 13 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v
index 3110da36a6..c2af667247 100644
--- a/theories/Numbers/Natural/Binary/NBinDefs.v
+++ b/theories/Numbers/Natural/Binary/NBinDefs.v
@@ -8,7 +8,7 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i i*)
+(*i $Id$ i*)
Require Import BinPos.
Require Export BinNat.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index bf4432c38a..558f2d0e49 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -1,3 +1,15 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(* Evgeny Makarov, INRIA, 2007 *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
Require Export NBinDefs.
Require Export NArithRing.