aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Natural/Abstract
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
-rw-r--r--theories/Numbers/Natural/Abstract/NAdd.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NAddOrder.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NAxioms.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NBase.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NDefOps.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NIso.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NMulOrder.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NOrder.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NProperties.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NStrongRec.v2
-rw-r--r--theories/Numbers/Natural/Abstract/NSub.v2
11 files changed, 0 insertions, 22 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 9f0b54a6a..859641280 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NBase.
Module NAddPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v
index 0ce04e54e..67bc80850 100644
--- a/theories/Numbers/Natural/Abstract/NAddOrder.v
+++ b/theories/Numbers/Natural/Abstract/NAddOrder.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NOrder.
Module NAddOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 42016ab10..cd3d8f0a8 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NZAxioms.
Set Implicit Arguments.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 842f4bcf2..f26f56d0c 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export Decidable.
Require Export NAxioms.
Require Import NZProperties.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 22eb2cb34..2302e8d35 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Import Bool. (* To get the orb and negb function *)
Require Import RelationPairs.
Require Export NStrongRec.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 47bf38cba..12dcd3258 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Import NBase.
Module Homomorphism (N1 N2 : NAxiomsSig).
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index a2162b137..29d1838c2 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NAddOrder.
Module NMulOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 090c02ecf..9439e04f5 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NAdd.
Module NOrderPropFunct (Import N : NAxiomsSig').
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 9fc9b290e..eed7cac18 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NAxioms NMaxMin.
(** This functor summarizes all known facts about N.
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index cbbcdbff5..bd666bc8b 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
(** This file defined the strong (course-of-value, well-founded) recursion
and proves its properties *)
diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v
index 1df032ea3..7d3117fdb 100644
--- a/theories/Numbers/Natural/Abstract/NSub.v
+++ b/theories/Numbers/Natural/Abstract/NSub.v
@@ -8,8 +8,6 @@
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
-(*i $Id$ i*)
-
Require Export NMulOrder.
Module Type NSubPropFunct (Import N : NAxiomsSig').