From 7f416bad62c0a94a0ff2fbdb433d03f3d5366ad6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 15 Jun 2016 18:52:24 +0200 Subject: ssrmatching: giving proper credits to the original author(s) Following CeCILL-B 5.3.2, we are allowed to redistribute the software under the same license of Coq as long as we credit. --- COPYRIGHT | 1 + CREDITS | 3 + plugins/ssrmatching/CeCILL-B | 514 ------------------------------------ plugins/ssrmatching/ssrmatching.ml4 | 11 +- 4 files changed, 13 insertions(+), 516 deletions(-) delete mode 100644 plugins/ssrmatching/CeCILL-B diff --git a/COPYRIGHT b/COPYRIGHT index 006ce18f1..8c08e05e6 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -9,6 +9,7 @@ This product includes also software developed by Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) Pierre Corbineau, Radboud University, Nijmegen (declarative mode) John Harrison, University of Cambridge (csdp wrapper) + Georges Gonthier, Microsoft Research - Inria Joint Centre (plugins/ssrmatching) The file CREDITS contains a list of contributors. The credits section in the Reference Manual details contributions. diff --git a/CREDITS b/CREDITS index ace4648dc..c6848648e 100644 --- a/CREDITS +++ b/CREDITS @@ -54,6 +54,9 @@ plugins/setoid_ring developed by Benjamin Grégoire (INRIA-Everest, 2005-2006), Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) and Bruno Barras (INRIA LogiCal, 2005-2006), +plugins/ssrmatching + developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011), + and Enrico Tassi (Inria-Marelle, 2011-now) plugins/subtac developed by Matthieu Sozeau (LRI, 2005-2008) plugins/micromega diff --git a/plugins/ssrmatching/CeCILL-B b/plugins/ssrmatching/CeCILL-B deleted file mode 100644 index fe29f5c9a..000000000 --- a/plugins/ssrmatching/CeCILL-B +++ /dev/null @@ -1,514 +0,0 @@ -CeCILL-B FREE SOFTWARE LICENSE AGREEMENT - - - Notice - -This Agreement is a Free Software license agreement that is the result -of discussions between its authors in order to ensure compliance with -the two main principles guiding its drafting: - - * firstly, compliance with the principles governing the distribution - of Free Software: access to source code, broad rights granted to - users, - * secondly, the election of a governing law, French law, with which - it is conformant, both as regards the law of torts and - intellectual property law, and the protection that it offers to - both authors and holders of the economic rights over software. - -The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) -license are: - -Commissariat à l'Energie Atomique - CEA, a public scientific, technical -and industrial research establishment, having its principal place of -business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. - -Centre National de la Recherche Scientifique - CNRS, a public scientific -and technological establishment, having its principal place of business -at 3 rue Michel-Ange, 75794 Paris cedex 16, France. - -Institut National de Recherche en Informatique et en Automatique - -INRIA, a public scientific and technological establishment, having its -principal place of business at Domaine de Voluceau, Rocquencourt, BP -105, 78153 Le Chesnay cedex, France. - - - Preamble - -This Agreement is an open source software license intended to give users -significant freedom to modify and redistribute the software licensed -hereunder. - -The exercising of this freedom is conditional upon a strong obligation -of giving credits for everybody that distributes a software -incorporating a software ruled by the current license so as all -contributions to be properly identified and acknowledged. - -In consideration of access to the source code and the rights to copy, -modify and redistribute granted by the license, users are provided only -with a limited warranty and the software's author, the holder of the -economic rights, and the successive licensors only have limited liability. - -In this respect, the risks associated with loading, using, modifying -and/or developing or reproducing the software by the user are brought to -the user's attention, given its Free Software status, which may make it -complicated to use, with the result that its use is reserved for -developers and experienced professionals having in-depth computer -knowledge. Users are therefore encouraged to load and test the -suitability of the software as regards their requirements in conditions -enabling the security of their systems and/or data to be ensured and, -more generally, to use and operate it in the same conditions of -security. This Agreement may be freely reproduced and published, -provided it is not altered, and that no provisions are either added or -removed herefrom. - -This Agreement may apply to any or all software for which the holder of -the economic rights decides to submit the use thereof to its provisions. - - - Article 1 - DEFINITIONS - -For the purpose of this Agreement, when the following expressions -commence with a capital letter, they shall have the following meaning: - -Agreement: means this license agreement, and its possible subsequent -versions and annexes. - -Software: means the software in its Object Code and/or Source Code form -and, where applicable, its documentation, "as is" when the Licensee -accepts the Agreement. - -Initial Software: means the Software in its Source Code and possibly its -Object Code form and, where applicable, its documentation, "as is" when -it is first distributed under the terms and conditions of the Agreement. - -Modified Software: means the Software modified by at least one -Contribution. - -Source Code: means all the Software's instructions and program lines to -which access is required so as to modify the Software. - -Object Code: means the binary files originating from the compilation of -the Source Code. - -Holder: means the holder(s) of the economic rights over the Initial -Software. - -Licensee: means the Software user(s) having accepted the Agreement. - -Contributor: means a Licensee having made at least one Contribution. - -Licensor: means the Holder, or any other individual or legal entity, who -distributes the Software under the Agreement. - -Contribution: means any or all modifications, corrections, translations, -adaptations and/or new functions integrated into the Software by any or -all Contributors, as well as any or all Internal Modules. - -Module: means a set of sources files including their documentation that -enables supplementary functions or services in addition to those offered -by the Software. - -External Module: means any or all Modules, not derived from the -Software, so that this Module and the Software run in separate address -spaces, with one calling the other when they are run. - -Internal Module: means any or all Module, connected to the Software so -that they both execute in the same address space. - -Parties: mean both the Licensee and the Licensor. - -These expressions may be used both in singular and plural form. - - - Article 2 - PURPOSE - -The purpose of the Agreement is the grant by the Licensor to the -Licensee of a non-exclusive, transferable and worldwide license for the -Software as set forth in Article 5 hereinafter for the whole term of the -protection granted by the rights over said Software. - - - Article 3 - ACCEPTANCE - -3.1 The Licensee shall be deemed as having accepted the terms and -conditions of this Agreement upon the occurrence of the first of the -following events: - - * (i) loading the Software by any or all means, notably, by - downloading from a remote server, or by loading from a physical - medium; - * (ii) the first time the Licensee exercises any of the rights - granted hereunder. - -3.2 One copy of the Agreement, containing a notice relating to the -characteristics of the Software, to the limited warranty, and to the -fact that its use is restricted to experienced users has been provided -to the Licensee prior to its acceptance as set forth in Article 3.1 -hereinabove, and the Licensee hereby acknowledges that it has read and -understood it. - - - Article 4 - EFFECTIVE DATE AND TERM - - - 4.1 EFFECTIVE DATE - -The Agreement shall become effective on the date when it is accepted by -the Licensee as set forth in Article 3.1. - - - 4.2 TERM - -The Agreement shall remain in force for the entire legal term of -protection of the economic rights over the Software. - - - Article 5 - SCOPE OF RIGHTS GRANTED - -The Licensor hereby grants to the Licensee, who accepts, the following -rights over the Software for any or all use, and for the term of the -Agreement, on the basis of the terms and conditions set forth hereinafter. - -Besides, if the Licensor owns or comes to own one or more patents -protecting all or part of the functions of the Software or of its -components, the Licensor undertakes not to enforce the rights granted by -these patents against successive Licensees using, exploiting or -modifying the Software. If these patents are transferred, the Licensor -undertakes to have the transferees subscribe to the obligations set -forth in this paragraph. - - - 5.1 RIGHT OF USE - -The Licensee is authorized to use the Software, without any limitation -as to its fields of application, with it being hereinafter specified -that this comprises: - - 1. permanent or temporary reproduction of all or part of the Software - by any or all means and in any or all form. - - 2. loading, displaying, running, or storing the Software on any or - all medium. - - 3. entitlement to observe, study or test its operation so as to - determine the ideas and principles behind any or all constituent - elements of said Software. This shall apply when the Licensee - carries out any or all loading, displaying, running, transmission - or storage operation as regards the Software, that it is entitled - to carry out hereunder. - - - 5.2 ENTITLEMENT TO MAKE CONTRIBUTIONS - -The right to make Contributions includes the right to translate, adapt, -arrange, or make any or all modifications to the Software, and the right -to reproduce the resulting software. - -The Licensee is authorized to make any or all Contributions to the -Software provided that it includes an explicit notice that it is the -author of said Contribution and indicates the date of the creation thereof. - - - 5.3 RIGHT OF DISTRIBUTION - -In particular, the right of distribution includes the right to publish, -transmit and communicate the Software to the general public on any or -all medium, and by any or all means, and the right to market, either in -consideration of a fee, or free of charge, one or more copies of the -Software by any means. - -The Licensee is further authorized to distribute copies of the modified -or unmodified Software to third parties according to the terms and -conditions set forth hereinafter. - - - 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION - -The Licensee is authorized to distribute true copies of the Software in -Source Code or Object Code form, provided that said distribution -complies with all the provisions of the Agreement and is accompanied by: - - 1. a copy of the Agreement, - - 2. a notice relating to the limitation of both the Licensor's - warranty and liability as set forth in Articles 8 and 9, - -and that, in the event that only the Object Code of the Software is -redistributed, the Licensee allows effective access to the full Source -Code of the Software at a minimum during the entire period of its -distribution of the Software, it being understood that the additional -cost of acquiring the Source Code shall not exceed the cost of -transferring the data. - - - 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE - -If the Licensee makes any Contribution to the Software, the resulting -Modified Software may be distributed under a license agreement other -than this Agreement subject to compliance with the provisions of Article -5.3.4. - - - 5.3.3 DISTRIBUTION OF EXTERNAL MODULES - -When the Licensee has developed an External Module, the terms and -conditions of this Agreement do not apply to said External Module, that -may be distributed under a separate license agreement. - - - 5.3.4 CREDITS - -Any Licensee who may distribute a Modified Software hereby expressly -agrees to: - - 1. indicate in the related documentation that it is based on the - Software licensed hereunder, and reproduce the intellectual - property notice for the Software, - - 2. ensure that written indications of the Software intended use, - intellectual property notice and license hereunder are included in - easily accessible format from the Modified Software interface, - - 3. mention, on a freely accessible website describing the Modified - Software, at least throughout the distribution term thereof, that - it is based on the Software licensed hereunder, and reproduce the - Software intellectual property notice, - - 4. where it is distributed to a third party that may distribute a - Modified Software without having to make its source code - available, make its best efforts to ensure that said third party - agrees to comply with the obligations set forth in this Article . - -If the Software, whether or not modified, is distributed with an -External Module designed for use in connection with the Software, the -Licensee shall submit said External Module to the foregoing obligations. - - - 5.3.5 COMPATIBILITY WITH THE CeCILL AND CeCILL-C LICENSES - -Where a Modified Software contains a Contribution subject to the CeCILL -license, the provisions set forth in Article 5.3.4 shall be optional. - -A Modified Software may be distributed under the CeCILL-C license. In -such a case the provisions set forth in Article 5.3.4 shall be optional. - - - Article 6 - INTELLECTUAL PROPERTY - - - 6.1 OVER THE INITIAL SOFTWARE - -The Holder owns the economic rights over the Initial Software. Any or -all use of the Initial Software is subject to compliance with the terms -and conditions under which the Holder has elected to distribute its work -and no one shall be entitled to modify the terms and conditions for the -distribution of said Initial Software. - -The Holder undertakes that the Initial Software will remain ruled at -least by this Agreement, for the duration set forth in Article 4.2. - - - 6.2 OVER THE CONTRIBUTIONS - -The Licensee who develops a Contribution is the owner of the -intellectual property rights over this Contribution as defined by -applicable law. - - - 6.3 OVER THE EXTERNAL MODULES - -The Licensee who develops an External Module is the owner of the -intellectual property rights over this External Module as defined by -applicable law and is free to choose the type of agreement that shall -govern its distribution. - - - 6.4 JOINT PROVISIONS - -The Licensee expressly undertakes: - - 1. not to remove, or modify, in any manner, the intellectual property - notices attached to the Software; - - 2. to reproduce said notices, in an identical manner, in the copies - of the Software modified or not. - -The Licensee undertakes not to directly or indirectly infringe the -intellectual property rights of the Holder and/or Contributors on the -Software and to take, where applicable, vis-à-vis its staff, any and all -measures required to ensure respect of said intellectual property rights -of the Holder and/or Contributors. - - - Article 7 - RELATED SERVICES - -7.1 Under no circumstances shall the Agreement oblige the Licensor to -provide technical assistance or maintenance services for the Software. - -However, the Licensor is entitled to offer this type of services. The -terms and conditions of such technical assistance, and/or such -maintenance, shall be set forth in a separate instrument. Only the -Licensor offering said maintenance and/or technical assistance services -shall incur liability therefor. - -7.2 Similarly, any Licensor is entitled to offer to its licensees, under -its sole responsibility, a warranty, that shall only be binding upon -itself, for the redistribution of the Software and/or the Modified -Software, under terms and conditions that it is free to decide. Said -warranty, and the financial terms and conditions of its application, -shall be subject of a separate instrument executed between the Licensor -and the Licensee. - - - Article 8 - LIABILITY - -8.1 Subject to the provisions of Article 8.2, the Licensee shall be -entitled to claim compensation for any direct loss it may have suffered -from the Software as a result of a fault on the part of the relevant -Licensor, subject to providing evidence thereof. - -8.2 The Licensor's liability is limited to the commitments made under -this Agreement and shall not be incurred as a result of in particular: -(i) loss due the Licensee's total or partial failure to fulfill its -obligations, (ii) direct or consequential loss that is suffered by the -Licensee due to the use or performance of the Software, and (iii) more -generally, any consequential loss. In particular the Parties expressly -agree that any or all pecuniary or business loss (i.e. loss of data, -loss of profits, operating loss, loss of customers or orders, -opportunity cost, any disturbance to business activities) or any or all -legal proceedings instituted against the Licensee by a third party, -shall constitute consequential loss and shall not provide entitlement to -any or all compensation from the Licensor. - - - Article 9 - WARRANTY - -9.1 The Licensee acknowledges that the scientific and technical -state-of-the-art when the Software was distributed did not enable all -possible uses to be tested and verified, nor for the presence of -possible defects to be detected. In this respect, the Licensee's -attention has been drawn to the risks associated with loading, using, -modifying and/or developing and reproducing the Software which are -reserved for experienced users. - -The Licensee shall be responsible for verifying, by any or all means, -the suitability of the product for its requirements, its good working -order, and for ensuring that it shall not cause damage to either persons -or properties. - -9.2 The Licensor hereby represents, in good faith, that it is entitled -to grant all the rights over the Software (including in particular the -rights set forth in Article 5). - -9.3 The Licensee acknowledges that the Software is supplied "as is" by -the Licensor without any other express or tacit warranty, other than -that provided for in Article 9.2 and, in particular, without any warranty -as to its commercial value, its secured, safe, innovative or relevant -nature. - -Specifically, the Licensor does not warrant that the Software is free -from any error, that it will operate without interruption, that it will -be compatible with the Licensee's own equipment and software -configuration, nor that it will meet the Licensee's requirements. - -9.4 The Licensor does not either expressly or tacitly warrant that the -Software does not infringe any third party intellectual property right -relating to a patent, software or any other property right. Therefore, -the Licensor disclaims any and all liability towards the Licensee -arising out of any or all proceedings for infringement that may be -instituted in respect of the use, modification and redistribution of the -Software. Nevertheless, should such proceedings be instituted against -the Licensee, the Licensor shall provide it with technical and legal -assistance for its defense. Such technical and legal assistance shall be -decided on a case-by-case basis between the relevant Licensor and the -Licensee pursuant to a memorandum of understanding. The Licensor -disclaims any and all liability as regards the Licensee's use of the -name of the Software. No warranty is given as regards the existence of -prior rights over the name of the Software or as regards the existence -of a trademark. - - - Article 10 - TERMINATION - -10.1 In the event of a breach by the Licensee of its obligations -hereunder, the Licensor may automatically terminate this Agreement -thirty (30) days after notice has been sent to the Licensee and has -remained ineffective. - -10.2 A Licensee whose Agreement is terminated shall no longer be -authorized to use, modify or distribute the Software. However, any -licenses that it may have granted prior to termination of the Agreement -shall remain valid subject to their having been granted in compliance -with the terms and conditions hereof. - - - Article 11 - MISCELLANEOUS - - - 11.1 EXCUSABLE EVENTS - -Neither Party shall be liable for any or all delay, or failure to -perform the Agreement, that may be attributable to an event of force -majeure, an act of God or an outside cause, such as defective -functioning or interruptions of the electricity or telecommunications -networks, network paralysis following a virus attack, intervention by -government authorities, natural disasters, water damage, earthquakes, -fire, explosions, strikes and labor unrest, war, etc. - -11.2 Any failure by either Party, on one or more occasions, to invoke -one or more of the provisions hereof, shall under no circumstances be -interpreted as being a waiver by the interested Party of its right to -invoke said provision(s) subsequently. - -11.3 The Agreement cancels and replaces any or all previous agreements, -whether written or oral, between the Parties and having the same -purpose, and constitutes the entirety of the agreement between said -Parties concerning said purpose. No supplement or modification to the -terms and conditions hereof shall be effective as between the Parties -unless it is made in writing and signed by their duly authorized -representatives. - -11.4 In the event that one or more of the provisions hereof were to -conflict with a current or future applicable act or legislative text, -said act or legislative text shall prevail, and the Parties shall make -the necessary amendments so as to comply with said act or legislative -text. All other provisions shall remain effective. Similarly, invalidity -of a provision of the Agreement, for any reason whatsoever, shall not -cause the Agreement as a whole to be invalid. - - - 11.5 LANGUAGE - -The Agreement is drafted in both French and English and both versions -are deemed authentic. - - - Article 12 - NEW VERSIONS OF THE AGREEMENT - -12.1 Any person is authorized to duplicate and distribute copies of this -Agreement. - -12.2 So as to ensure coherence, the wording of this Agreement is -protected and may only be modified by the authors of the License, who -reserve the right to periodically publish updates or new versions of the -Agreement, each with a separate number. These subsequent versions may -address new issues encountered by Free Software. - -12.3 Any Software distributed under a given version of the Agreement may -only be subsequently distributed under the same version of the Agreement -or a subsequent version. - - - Article 13 - GOVERNING LAW AND JURISDICTION - -13.1 The Agreement is governed by French law. The Parties agree to -endeavor to seek an amicable solution to any disagreements or disputes -that may arise during the performance of the Agreement. - -13.2 Failing an amicable solution within two (2) months as from their -occurrence, and unless emergency proceedings are necessary, the -disagreements or disputes shall be referred to the Paris Courts having -jurisdiction, by the more diligent Party. - - -Version 1.0 dated 2006-09-05. diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 378403f8d..933e2baee 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1,5 +1,12 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(*