diff options
author | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-07-27 10:02:38 +0200 |
commit | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (patch) | |
tree | 8b5450c5801a1592e0348ad0362f950e7bb958d4 /plugins/ring | |
parent | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (diff) |
Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg
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 089dec02..0d92973e 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 7f1597a1..b358251a 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 d4f40081..31b7cd7c 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 09de1bb4..8f07ad26 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 3f01a5c3..472c91b4 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 a00b7bcd..4aec3893 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 d286208a..6306c4a7 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 4717edc9..4b484483 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 b0d790e0..e71be89a 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 52f5968b..bb88f646 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 8953b88f..f2e904b1 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \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 7b0d96bb..db88a05c 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___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |