aboutsummaryrefslogtreecommitdiff
path: root/theories/Num
diff options
context:
space:
mode:
authorfilliatr2001-03-15 13:38:59 +0000
committerfilliatr2001-03-15 13:38:59 +0000
commit187dc15532f0c6f380d7bcb07adc2180c29fedc2 (patch)
treed7bacf01519ca82b5745d2c493c7f7f1826106af /theories/Num
parent23741168b109daece8bb588b9c5fb4506e7726ce (diff)
entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Num')
-rw-r--r--theories/Num/AddProps.v7
-rw-r--r--theories/Num/Axioms.v7
-rw-r--r--theories/Num/Definitions.v7
-rw-r--r--theories/Num/DiscrAxioms.v7
-rw-r--r--theories/Num/DiscrProps.v7
-rw-r--r--theories/Num/GeAxioms.v7
-rw-r--r--theories/Num/GeProps.v7
-rw-r--r--theories/Num/GtAxioms.v7
-rw-r--r--theories/Num/GtProps.v7
-rw-r--r--theories/Num/LeAxioms.v7
-rw-r--r--theories/Num/LeProps.v7
-rw-r--r--theories/Num/LtProps.v7
-rw-r--r--theories/Num/NSyntax.v7
-rw-r--r--theories/Num/OppAxioms.v7
-rw-r--r--theories/Num/OppProps.v7
-rw-r--r--theories/Num/SubProps.v7
16 files changed, 112 insertions, 0 deletions
diff --git a/theories/Num/AddProps.v b/theories/Num/AddProps.v
index 87fba8eba9..cc48a87441 100644
--- a/theories/Num/AddProps.v
+++ b/theories/Num/AddProps.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
Require Export Axioms.
diff --git a/theories/Num/Axioms.v b/theories/Num/Axioms.v
index 7e65fc9476..c9ada6ebc6 100644
--- a/theories/Num/Axioms.v
+++ b/theories/Num/Axioms.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id: i*)
(*s Axioms for the basic numerical operations *)
diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v
index defb12897a..2b908f5cda 100644
--- a/theories/Num/Definitions.v
+++ b/theories/Num/Definitions.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id $ i*)
(*s
diff --git a/theories/Num/DiscrAxioms.v b/theories/Num/DiscrAxioms.v
index 42e58cd3c4..83b2e42f47 100644
--- a/theories/Num/DiscrAxioms.v
+++ b/theories/Num/DiscrAxioms.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id$ i*)
Require Export Params.
diff --git a/theories/Num/DiscrProps.v b/theories/Num/DiscrProps.v
index 7c84d2b354..5554357e8c 100644
--- a/theories/Num/DiscrProps.v
+++ b/theories/Num/DiscrProps.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id$ i*)
Require Export DiscrAxioms.
diff --git a/theories/Num/GeAxioms.v b/theories/Num/GeAxioms.v
index d5d2375e99..f242479758 100644
--- a/theories/Num/GeAxioms.v
+++ b/theories/Num/GeAxioms.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id: i*)
Require Export Axioms.
Require Export LtProps.
diff --git a/theories/Num/GeProps.v b/theories/Num/GeProps.v
index e69de29bb2..b5bc074d17 100644
--- a/theories/Num/GeProps.v
+++ b/theories/Num/GeProps.v
@@ -0,0 +1,7 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
diff --git a/theories/Num/GtAxioms.v b/theories/Num/GtAxioms.v
index 9a54a0988e..548d43cdf0 100644
--- a/theories/Num/GtAxioms.v
+++ b/theories/Num/GtAxioms.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id: i*)
Require Export Axioms.
Require Export LeProps.
diff --git a/theories/Num/GtProps.v b/theories/Num/GtProps.v
index e69de29bb2..b5bc074d17 100644
--- a/theories/Num/GtProps.v
+++ b/theories/Num/GtProps.v
@@ -0,0 +1,7 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
diff --git a/theories/Num/LeAxioms.v b/theories/Num/LeAxioms.v
index b71682e4fe..668c4677de 100644
--- a/theories/Num/LeAxioms.v
+++ b/theories/Num/LeAxioms.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*i $Id: i*)
Require Export Axioms.
Require Export LtProps.
diff --git a/theories/Num/LeProps.v b/theories/Num/LeProps.v
index 68f782e63e..c476bb2066 100644
--- a/theories/Num/LeProps.v
+++ b/theories/Num/LeProps.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
Require Export LtProps.
Require Export LeAxioms.
diff --git a/theories/Num/LtProps.v b/theories/Num/LtProps.v
index aeff45f29b..490fbbb128 100644
--- a/theories/Num/LtProps.v
+++ b/theories/Num/LtProps.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
Require Export Axioms.
Require Export AddProps.
diff --git a/theories/Num/NSyntax.v b/theories/Num/NSyntax.v
index 117832c01b..488f900e5b 100644
--- a/theories/Num/NSyntax.v
+++ b/theories/Num/NSyntax.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
(*s Syntax for arithmetic *)
diff --git a/theories/Num/OppAxioms.v b/theories/Num/OppAxioms.v
index e69de29bb2..b5bc074d17 100644
--- a/theories/Num/OppAxioms.v
+++ b/theories/Num/OppAxioms.v
@@ -0,0 +1,7 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
diff --git a/theories/Num/OppProps.v b/theories/Num/OppProps.v
index e69de29bb2..b5bc074d17 100644
--- a/theories/Num/OppProps.v
+++ b/theories/Num/OppProps.v
@@ -0,0 +1,7 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
diff --git a/theories/Num/SubProps.v b/theories/Num/SubProps.v
index e69de29bb2..b5bc074d17 100644
--- a/theories/Num/SubProps.v
+++ b/theories/Num/SubProps.v
@@ -0,0 +1,7 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-18 21:25:26 +0000