diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-24 15:57:30 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-24 15:57:30 +0000 |
commit | 8d99bfcdc0915c006bffba6d5ffe14c683b9eb65 (patch) | |
tree | f66bf6b10fae56354ae82f811c2a8273d5d30e13 /plugins/ring | |
parent | 27882e4edd07e306333fdc024330982741416a19 (diff) |
Updated all headers for 8.3 and trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/ring')
-rw-r--r-- | plugins/ring/LegacyArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyNArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyRing_theory.v | 2 | ||||
-rw-r--r-- | plugins/ring/LegacyZArithRing.v | 2 | ||||
-rw-r--r-- | plugins/ring/Ring_abstract.v | 2 | ||||
-rw-r--r-- | plugins/ring/Ring_normalize.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_normalize.v | 2 | ||||
-rw-r--r-- | plugins/ring/Setoid_ring_theory.v | 2 | ||||
-rw-r--r-- | plugins/ring/g_ring.ml4 | 2 | ||||
-rw-r--r-- | plugins/ring/ring.ml | 2 |
12 files changed, 12 insertions, 12 deletions
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v index 9572c1ce7..9259d490f 100644 --- a/plugins/ring/LegacyArithRing.v +++ b/plugins/ring/LegacyArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v index eb62def87..fa7709982 100644 --- a/plugins/ring/LegacyNArithRing.v +++ b/plugins/ring/LegacyNArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v index cd51f9e02..d19e9f589 100644 --- a/plugins/ring/LegacyRing.v +++ b/plugins/ring/LegacyRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v index a3071f7b4..ca3355a6e 100644 --- a/plugins/ring/LegacyRing_theory.v +++ b/plugins/ring/LegacyRing_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v index c48d61b0d..87b64c8d8 100644 --- a/plugins/ring/LegacyZArithRing.v +++ b/plugins/ring/LegacyZArithRing.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v index cccfe653b..e009f14ea 100644 --- a/plugins/ring/Ring_abstract.v +++ b/plugins/ring/Ring_abstract.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v index 54ddcb9ae..073cd2f63 100644 --- a/plugins/ring/Ring_normalize.v +++ b/plugins/ring/Ring_normalize.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v index 127228116..106a946d3 100644 --- a/plugins/ring/Setoid_ring.v +++ b/plugins/ring/Setoid_ring.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v index 8d77854b6..d157bffce 100644 --- a/plugins/ring/Setoid_ring_normalize.v +++ b/plugins/ring/Setoid_ring_normalize.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v index 0444fe74a..dd722f801 100644 --- a/plugins/ring/Setoid_ring_theory.v +++ b/plugins/ring/Setoid_ring_theory.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4 index 99650a32f..e306a5319 100644 --- a/plugins/ring/g_ring.ml4 +++ b/plugins/ring/g_ring.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 81f6b66ee..8b977e5dc 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |