diff options
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$ *) |