diff options
| author | filliatr | 2001-03-15 13:38:59 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-15 13:38:59 +0000 |
| commit | 187dc15532f0c6f380d7bcb07adc2180c29fedc2 (patch) | |
| tree | d7bacf01519ca82b5745d2c493c7f7f1826106af /contrib/ring | |
| parent | 23741168b109daece8bb588b9c5fb4506e7726ce (diff) | |
entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/ring')
| -rw-r--r-- | contrib/ring/ArithRing.v | 7 | ||||
| -rw-r--r-- | contrib/ring/Quote.v | 7 | ||||
| -rw-r--r-- | contrib/ring/Ring.v | 7 | ||||
| -rw-r--r-- | contrib/ring/Ring_abstract.v | 7 | ||||
| -rw-r--r-- | contrib/ring/Ring_normalize.v | 7 | ||||
| -rw-r--r-- | contrib/ring/Ring_theory.v | 7 | ||||
| -rw-r--r-- | contrib/ring/ZArithRing.v | 7 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 7 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 7 |
9 files changed, 63 insertions, 0 deletions
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v index 14d69e2b02..0dfb1f4e35 100644 --- a/contrib/ring/ArithRing.v +++ b/contrib/ring/ArithRing.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v index e7c995cf3b..f97c81c408 100644 --- a/contrib/ring/Quote.v +++ b/contrib/ring/Quote.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index b6f75a5841..c94dce065e 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v index 6bb1f5aa9a..7626899850 100644 --- a/contrib/ring/Ring_abstract.v +++ b/contrib/ring/Ring_abstract.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v index 536d2d3034..94b5093c70 100644 --- a/contrib/ring/Ring_normalize.v +++ b/contrib/ring/Ring_normalize.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v index c04eee57ec..867ab22fbe 100644 --- a/contrib/ring/Ring_theory.v +++ b/contrib/ring/Ring_theory.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v index a8adfe2f63..2de8611764 100644 --- a/contrib/ring/ZArithRing.v +++ b/contrib/ring/ZArithRing.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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index ac3af30b8d..c82ccecb00 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -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 *) +(***********************************************************************) (* $Id$ *) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 0e200313c7..589c1580ea 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -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 *) +(***********************************************************************) (* $Id$ *) |