summaryrefslogtreecommitdiff
path: root/theories/Arith
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Arith')
-rw-r--r--theories/Arith/Arith.v2
-rw-r--r--theories/Arith/Arith_base.v2
-rw-r--r--theories/Arith/Between.v2
-rw-r--r--theories/Arith/Bool_nat.v2
-rw-r--r--theories/Arith/Compare.v2
-rw-r--r--theories/Arith/Compare_dec.v2
-rw-r--r--theories/Arith/Div2.v2
-rw-r--r--theories/Arith/EqNat.v2
-rw-r--r--theories/Arith/Euclid.v2
-rw-r--r--theories/Arith/Even.v2
-rw-r--r--theories/Arith/Factorial.v2
-rw-r--r--theories/Arith/Gt.v2
-rw-r--r--theories/Arith/Le.v2
-rw-r--r--theories/Arith/Lt.v2
-rw-r--r--theories/Arith/Max.v2
-rw-r--r--theories/Arith/Min.v2
-rw-r--r--theories/Arith/Minus.v2
-rw-r--r--theories/Arith/Mult.v2
-rw-r--r--theories/Arith/Peano_dec.v2
-rw-r--r--theories/Arith/Plus.v2
-rw-r--r--theories/Arith/Wf_nat.v2
21 files changed, 21 insertions, 21 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v
index 3cf607d9..0f5ef9d0 100644
--- a/theories/Arith/Arith.v
+++ b/theories/Arith/Arith.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Arith.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Export Arith_base.
Require Export ArithRing.
diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v
index e975f273..c5135f63 100644
--- a/theories/Arith/Arith_base.v
+++ b/theories/Arith/Arith_base.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Arith_base.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Export Le.
Require Export Lt.
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index 8ab49f25..2ccf802d 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Between.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Le.
Require Import Lt.
diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v
index 5904e989..9ace38b1 100644
--- a/theories/Arith/Bool_nat.v
+++ b/theories/Arith/Bool_nat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Bool_nat.v 13323 2010-07-24 15:57:30Z herbelin $ *)
Require Export Compare_dec.
Require Export Peano_dec.
diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v
index cdba76eb..2775d132 100644
--- a/theories/Arith/Compare.v
+++ b/theories/Arith/Compare.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Compare.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Equality is decidable on [nat] *)
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 5d20261c..0811fea7 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Compare_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Le.
Require Import Lt.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 0a3b7dcc..adbca442 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Div2.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Lt.
Require Import Plus.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index edf31c62..e49e5d14 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: EqNat.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Equality on natural numbers *)
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v
index 78185715..54f4f013 100644
--- a/theories/Arith/Euclid.v
+++ b/theories/Arith/Euclid.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Euclid.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Mult.
Require Import Compare_dec.
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v
index 266d51fc..527ad748 100644
--- a/theories/Arith/Even.v
+++ b/theories/Arith/Even.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Even.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Here we define the predicates [even] and [odd] by mutual induction
and we prove the decidability and the exclusion of those predicates.
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index aa8bb7bd..5385bf61 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Factorial.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Plus.
Require Import Mult.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index bcf38c02..eda051df 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Gt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as:
<<
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index a8b86ab7..f24667d0 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Le.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Order on natural numbers. [le] is defined in [Init/Peano.v] as:
<<
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index 68ac6e73..0032741e 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Lt.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as:
<<
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 3a566321..b4c4d7ad 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Max.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v
index f646c80a..81142249 100644
--- a/theories/Arith/Min.v
+++ b/theories/Arith/Min.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Min.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *)
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 74d2c9a8..39062348 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Minus.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as:
<<
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index bfefb967..3ba98472 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Mult.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Export Plus.
Require Export Minus.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 5eb86168..908f99f0 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Peano_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
Require Import Decidable.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 2ea65696..3c5f28b6 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Plus.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Properties of addition. [add] is defined in [Init/Peano.v] as:
<<
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index a42c38eb..07ab1c3e 100644
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id$ i*)
+(*i $Id: Wf_nat.v 13323 2010-07-24 15:57:30Z herbelin $ i*)
(** Well-founded relations and natural numbers *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 04:05:03 +0000