diff options
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/BinInt.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Int.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Wf_Z.v | 2 | ||||
-rw-r--r-- | theories/ZArith/ZArith.v | 2 | ||||
-rw-r--r-- | theories/ZArith/ZArith_base.v | 2 | ||||
-rw-r--r-- | theories/ZArith/ZArith_dec.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zabs.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zbool.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zcomplements.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zdigits.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zdiv.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zeven.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zgcd_alt.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zhints.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zlogarithm.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zmax.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zmin.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zmisc.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Znat.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Znumtheory.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zorder.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zpow_facts.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zpower.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zsqrt.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zwf.v | 2 | ||||
-rw-r--r-- | theories/ZArith/auxiliary.v | 2 |
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) *) |