aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic
diff options
context:
space:
mode:
authorletouzey2010-04-29 13:50:31 +0000
committerletouzey2010-04-29 13:50:31 +0000
commitaf93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch)
treeb9a4f28e6f8106bcf19e017f64147f836f810c4b /theories/Numbers/Cyclic
parent0f61b02f84b41e1f019cd78824de28f18ff854aa (diff)
Remove the svn-specific $Id$ annotations
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v2
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v2
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v2
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v2
-rw-r--r--theories/Numbers/Cyclic/Int31/Int31.v2
-rw-r--r--theories/Numbers/Cyclic/Int31/Ring31.v2
-rw-r--r--theories/Numbers/Cyclic/ZModulo/ZModulo.v2
16 files changed, 0 insertions, 32 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index af30b0175b..0403722cb3 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(* $Id$ *)
-
(** * Signature and specification of a bounded integer structure *)
(** This file specifies how to represent [Z/nZ] when [n=2^d],
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index b68e89560e..0796d9f49b 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NZAxioms.
Require Import BigNumPrelude.
Require Import DoubleType.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index aa798e1c7f..81b2c9403f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
index 23c62740c8..bf18c1753d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 49a4f950a8..a640aaf7f9 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index 1ce1e81b0c..ae806dd5e4 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
index 136f96c043..1c4247231f 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
index 3405b6f4d6..1395caa338 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
index 6a2a344490..8b978172c0 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index e2c6232013..81df55bd44 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
index a7e556713a..a5610fe783 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 88cbb484fc..da75219a5b 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Set Implicit Arguments.
Require Import ZArith.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index e2e5b563f2..ca73a9f005 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
(**
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index cc224254f8..9b4c25e2c2 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -8,8 +8,6 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Import NaryFunctions.
Require Import Wf_nat.
Require Export ZArith.
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index a9c499fb95..01002656df 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
(** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped
with a ring structure and a ring tactic *)
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index da0be5e2ab..a2ee248ab0 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
-
(** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ]
as defined abstractly in CyclicAxioms. *)