From 4a816963c315007576bfaba3e87df0c7091e1402 Mon Sep 17 00:00:00 2001
From: mohring
Date: Thu, 19 Apr 2001 12:41:04 +0000
Subject: Mise de (*i autour CVS info

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/IntMap/Adalloc.v   | 8 ++++++++
 theories/IntMap/Addec.v     | 8 ++++++++
 theories/IntMap/Addr.v      | 8 ++++++++
 theories/IntMap/Adist.v     | 8 ++++++++
 theories/IntMap/Allmaps.v   | 8 ++++++++
 theories/IntMap/Fset.v      | 8 ++++++++
 theories/IntMap/Lsort.v     | 8 ++++++++
 theories/IntMap/Map.v       | 8 ++++++++
 theories/IntMap/Mapaxioms.v | 8 ++++++++
 theories/IntMap/Mapc.v      | 8 ++++++++
 theories/IntMap/Mapcanon.v  | 8 ++++++++
 theories/IntMap/Mapcard.v   | 8 ++++++++
 theories/IntMap/Mapfold.v   | 8 ++++++++
 theories/IntMap/Mapiter.v   | 8 ++++++++
 theories/IntMap/Maplists.v  | 8 ++++++++
 theories/IntMap/Mapsubset.v | 8 ++++++++
 theories/IntMap/intro.tex   | 3 ++-
 17 files changed, 130 insertions(+), 1 deletion(-)

(limited to 'theories/IntMap')

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 47cff4f8e9..63c2f2ad4b 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 889c38d950..abbe450816 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Equality on adresses *)
 Require Bool.
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 1623e914b0..debaed16cf 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Representation of adresses by [positive] the type of binary numbers *)
 
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index f8bae6853c..f5d40e66f8 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require ZArith.
diff --git a/theories/IntMap/Allmaps.v b/theories/IntMap/Allmaps.v
index 89520483ba..fcd111694d 100644
--- a/theories/IntMap/Allmaps.v
+++ b/theories/IntMap/Allmaps.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Export Addr.
 Require Export Adist.
diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 743c703b27..130e89edc4 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Sets operations on maps *)
 
diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v
index 63a2afa61e..7f8e61e600 100644
--- a/theories/IntMap/Lsort.v
+++ b/theories/IntMap/Lsort.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index ca436cddb5..a9093f08d7 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 (*s Definition of finite sets as trees indexed by adresses *)
 
diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v
index 638a833d7c..957f25e1f0 100644
--- a/theories/IntMap/Mapaxioms.v
+++ b/theories/IntMap/Mapaxioms.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index 4d9d26ff39..d78c05d6b9 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index b0fc1303db..b1616ebeb8 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index ce2a042c99..51c92c2bc5 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
index ac959bdd85..46b0fb2c72 100644
--- a/theories/IntMap/Mapfold.v
+++ b/theories/IntMap/Mapfold.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v
index 43f4ffecaf..39ea1d9d8a 100644
--- a/theories/IntMap/Mapiter.v
+++ b/theories/IntMap/Mapiter.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v
index 8a920c68c7..c36c021511 100644
--- a/theories/IntMap/Maplists.v
+++ b/theories/IntMap/Maplists.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Addr.
 Require Addec.
diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index c7cc430bf8..5cbfe7ef76 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -1,3 +1,11 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(*i 	$Id$	 i*)
 
 Require Bool.
 Require Sumbool.
diff --git a/theories/IntMap/intro.tex b/theories/IntMap/intro.tex
index cfaae2468b..9ad93050c1 100644
--- a/theories/IntMap/intro.tex
+++ b/theories/IntMap/intro.tex
@@ -1,5 +1,6 @@
-\section{IntMap}\label{IntMap}
+\section{Maps indexed by binary integers : IntMap}\label{IntMap}
 
 This library contains a data structure for finite sets implemented by
 an efficient structure of map (trees indexed by binary integers).
+It was initially developed by Jean Goubault.
 
-- 
cgit v1.2.3