summaryrefslogtreecommitdiff
path: root/theories/ZArith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith')
-rw-r--r--theories/ZArith/BinInt.v2
-rw-r--r--theories/ZArith/Int.v2
-rw-r--r--theories/ZArith/Wf_Z.v2
-rw-r--r--theories/ZArith/ZArith.v2
-rw-r--r--theories/ZArith/ZArith_base.v2
-rw-r--r--theories/ZArith/ZArith_dec.v2
-rw-r--r--theories/ZArith/Zabs.v2
-rw-r--r--theories/ZArith/Zbool.v2
-rw-r--r--theories/ZArith/Zcomplements.v2
-rw-r--r--theories/ZArith/Zdigits.v2
-rw-r--r--theories/ZArith/Zdiv.v2
-rw-r--r--theories/ZArith/Zeven.v2
-rw-r--r--theories/ZArith/Zgcd_alt.v2
-rw-r--r--theories/ZArith/Zhints.v2
-rw-r--r--theories/ZArith/Zlogarithm.v2
-rw-r--r--theories/ZArith/Zmax.v2
-rw-r--r--theories/ZArith/Zmin.v2
-rw-r--r--theories/ZArith/Zmisc.v2
-rw-r--r--theories/ZArith/Znat.v2
-rw-r--r--theories/ZArith/Znumtheory.v2
-rw-r--r--theories/ZArith/Zorder.v2
-rw-r--r--theories/ZArith/Zpow_facts.v2
-rw-r--r--theories/ZArith/Zpower.v2
-rw-r--r--theories/ZArith/Zsqrt.v2
-rw-r--r--theories/ZArith/Zwf.v2
-rw-r--r--theories/ZArith/auxiliary.v2
26 files changed, 26 insertions, 26 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 5dbeffa4..2a615311 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(***********************************************************)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 30c08fdc..c0123ca8 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id$ *)
+(* $Id: Int.v 12363 2009-09-28 15:04:07Z letouzey $ *)
(** * An light axiomatization of integers (used in FSetAVL). *)
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index f073463f..d449100c 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Wf_Z.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import BinInt.
Require Import Zcompare.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index e3937278..96d42077 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: ZArith.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Library for manipulating integers based on binary encoding *)
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 6a60a021..4af8eb8f 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: ZArith_base.v 13323 2010-07-24 15:57:30Z herbelin $ *)
(** Library for manipulating integers based on binary encoding.
These are the basic modules, required by [Omega] and [Ring] for instance.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index c4d7cef4..1c5efb07 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: ZArith_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Sumbool.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 2c1b8e74..0057c29c 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -6,7 +6,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zabs.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index fcc2f5b8..79cef8f9 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Zbool.v 13323 2010-07-24 15:57:30Z herbelin $ *)
Require Import BinInt.
Require Import Zeven.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index d8a5781c..2163e211 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zcomplements.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import ZArithRing.
Require Import ZArith_base.
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index 71466e9e..78a78007 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zdigits.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Bit vectors interpreted as integers.
Contribution by Jean Duprat (ENS Lyon). *)
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 78dd7050..0f2268cd 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zdiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(* Contribution by Claude Marché and Xavier Urbain *)
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index d4fdaca8..3923d8aa 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zeven.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import BinInt.
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index e5767ddd..26c3c0c2 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zgcd_alt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *)
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index f41e2f01..5dd8c23c 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zhints.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** This file centralizes the lemmas about [Z], classifying them
according to the way they can be used in automatic search *)
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 0666380a..67650b0c 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zlogarithm.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(**********************************************************************)
(** The integer logarithms with base 2.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 48b9c858..7285ec5a 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zmax.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index f9b23fde..5b1564d6 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zmin.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 50d4c7f8..f625f762 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zmisc.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Wf_nat.
Require Import BinInt.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index cd258af3..0feb4df1 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Znat.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 4347d70c..c3394ed4 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Znumtheory.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import ZArith_base.
Require Import ZArithRing.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 13112e01..a691d269 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -6,7 +6,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zorder.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 84b49799..226a573c 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zpow_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import ZArith_base.
Require Import ZArithRing.
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 6e30ca08..e7c2fc57 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Zpower.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Wf_nat.
Require Import ZArith_base.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 1e9db3d1..8d4f70e9 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Zsqrt.v 13323 2010-07-24 15:57:30Z herbelin $ *)
Require Import ZArithRing.
Require Import Omega.
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 03678a27..cc4687ee 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Zwf.v 13323 2010-07-24 15:57:30Z herbelin $ *)
Require Import ZArith_base.
Require Export Wf_nat.
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index bd2033b8..f50e7bf7 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: auxiliary.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 16:08:26 +0000