aboutsummaryrefslogtreecommitdiff
path: root/theories/IntMap
diff options
context:
space:
mode:
authormohring2001-04-19 12:41:04 +0000
committermohring2001-04-19 12:41:04 +0000
commit4a816963c315007576bfaba3e87df0c7091e1402 (patch)
tree9b32d023e23b3c9cfa2b11382c34796aa3630b87 /theories/IntMap
parentbdbbb1bea47909ad5d0daffd77e090ef9b59d826 (diff)
Mise de (*i autour CVS info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1620 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/IntMap')
-rw-r--r--theories/IntMap/Adalloc.v8
-rw-r--r--theories/IntMap/Addec.v8
-rw-r--r--theories/IntMap/Addr.v8
-rw-r--r--theories/IntMap/Adist.v8
-rw-r--r--theories/IntMap/Allmaps.v8
-rw-r--r--theories/IntMap/Fset.v8
-rw-r--r--theories/IntMap/Lsort.v8
-rw-r--r--theories/IntMap/Map.v8
-rw-r--r--theories/IntMap/Mapaxioms.v8
-rw-r--r--theories/IntMap/Mapc.v8
-rw-r--r--theories/IntMap/Mapcanon.v8
-rw-r--r--theories/IntMap/Mapcard.v8
-rw-r--r--theories/IntMap/Mapfold.v8
-rw-r--r--theories/IntMap/Mapiter.v8
-rw-r--r--theories/IntMap/Maplists.v8
-rw-r--r--theories/IntMap/Mapsubset.v8
-rw-r--r--theories/IntMap/intro.tex3
17 files changed, 130 insertions, 1 deletions
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 13:15:40 +0000