summaryrefslogtreecommitdiff
path: root/theories/IntMap
diff options
context:
space:
mode:
Diffstat (limited to 'theories/IntMap')
-rw-r--r--theories/IntMap/Adalloc.v2
-rw-r--r--theories/IntMap/Addec.v2
-rw-r--r--theories/IntMap/Addr.v2
-rw-r--r--theories/IntMap/Adist.v2
-rw-r--r--theories/IntMap/Allmaps.v2
-rw-r--r--theories/IntMap/Fset.v2
-rw-r--r--theories/IntMap/Lsort.v2
-rw-r--r--theories/IntMap/Map.v2
-rw-r--r--theories/IntMap/Mapaxioms.v2
-rw-r--r--theories/IntMap/Mapc.v2
-rw-r--r--theories/IntMap/Mapcanon.v2
-rw-r--r--theories/IntMap/Mapcard.v2
-rw-r--r--theories/IntMap/Mapfold.v2
-rw-r--r--theories/IntMap/Mapiter.v2
-rw-r--r--theories/IntMap/Maplists.v2
-rw-r--r--theories/IntMap/Mapsubset.v2
16 files changed, 16 insertions, 16 deletions
diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
index 9fde8f5f..2136bfb5 100644
--- a/theories/IntMap/Adalloc.v
+++ b/theories/IntMap/Adalloc.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Adalloc.v,v 1.10.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Adalloc.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
index 7dba9ef6..f1a937a3 100644
--- a/theories/IntMap/Addec.v
+++ b/theories/IntMap/Addec.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Addec.v,v 1.7.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Addec.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Equality on adresses *)
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v
index 1370d72d..727117b3 100644
--- a/theories/IntMap/Addr.v
+++ b/theories/IntMap/Addr.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Addr.v,v 1.8.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Addr.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Representation of adresses by the [positive] type of binary numbers *)
diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index cdb4c885..790218ce 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Adist.v,v 1.9.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Adist.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import ZArith.
diff --git a/theories/IntMap/Allmaps.v b/theories/IntMap/Allmaps.v
index 68744220..f9a0feac 100644
--- a/theories/IntMap/Allmaps.v
+++ b/theories/IntMap/Allmaps.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Allmaps.v,v 1.3.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Allmaps.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Export Addr.
Require Export Adist.
diff --git a/theories/IntMap/Fset.v b/theories/IntMap/Fset.v
index 8d217be9..27f739c1 100644
--- a/theories/IntMap/Fset.v
+++ b/theories/IntMap/Fset.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Fset.v,v 1.5.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Fset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(*s Sets operations on maps *)
diff --git a/theories/IntMap/Lsort.v b/theories/IntMap/Lsort.v
index 48972872..d31d8133 100644
--- a/theories/IntMap/Lsort.v
+++ b/theories/IntMap/Lsort.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Lsort.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Lsort.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Map.v b/theories/IntMap/Map.v
index da1fa99e..5345f81b 100644
--- a/theories/IntMap/Map.v
+++ b/theories/IntMap/Map.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Map.v,v 1.7.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Map.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
(** Definition of finite sets as trees indexed by adresses *)
diff --git a/theories/IntMap/Mapaxioms.v b/theories/IntMap/Mapaxioms.v
index 9d09f2a9..b6a2b134 100644
--- a/theories/IntMap/Mapaxioms.v
+++ b/theories/IntMap/Mapaxioms.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapaxioms.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapaxioms.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v
index 7a394abb..d7a779ff 100644
--- a/theories/IntMap/Mapc.v
+++ b/theories/IntMap/Mapc.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapc.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapc.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Mapcanon.v b/theories/IntMap/Mapcanon.v
index 868fbe5e..23e0669e 100644
--- a/theories/IntMap/Mapcanon.v
+++ b/theories/IntMap/Mapcanon.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapcanon.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapcanon.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Mapcard.v b/theories/IntMap/Mapcard.v
index 49f9fe91..35efac47 100644
--- a/theories/IntMap/Mapcard.v
+++ b/theories/IntMap/Mapcard.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapcard.v,v 1.5.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapcard.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Mapfold.v b/theories/IntMap/Mapfold.v
index 641529ee..335a1384 100644
--- a/theories/IntMap/Mapfold.v
+++ b/theories/IntMap/Mapfold.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapfold.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapfold.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Mapiter.v b/theories/IntMap/Mapiter.v
index f5d443cc..31e98c49 100644
--- a/theories/IntMap/Mapiter.v
+++ b/theories/IntMap/Mapiter.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapiter.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Mapiter.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
diff --git a/theories/IntMap/Maplists.v b/theories/IntMap/Maplists.v
index 645c3407..1d53e6e5 100644
--- a/theories/IntMap/Maplists.v
+++ b/theories/IntMap/Maplists.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Maplists.v,v 1.4.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
+(*i $Id: Maplists.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Addr.
Require Import Addec.
diff --git a/theories/IntMap/Mapsubset.v b/theories/IntMap/Mapsubset.v
index 33b412e3..e27943fb 100644
--- a/theories/IntMap/Mapsubset.v
+++ b/theories/IntMap/Mapsubset.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Mapsubset.v,v 1.4.2.1 2004/07/16 19:31:05 herbelin Exp $ i*)
+(*i $Id: Mapsubset.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
Require Import Bool.
Require Import Sumbool.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 07:34:03 +0000