ssreflect (1.11.0-1) unstable; urgency=medium

  * New upstream release
  * Debhelper compatibility level 13:
    -drop override of dh_missing which is no longer needed
  * Set Rules-Requires-Root to no

[dgit import unpatched ssreflect 1.11.0-1]

17 files changed, 1033 insertions, 0 deletions

diff --git a/debian/README.source b/debian/README.source
new file mode 100644
index 0000000..24e6695
--- /dev/null
+++ b/debian/README.source
@@ -0,0 +1,35 @@
+Ssreflect Debian source package
+===============================
+
+Packaging a new upstream
+------------------------
+
+ * Ssreflect uses internal structures of Coq and is quite easily
+   broken by new versions of Coq. However, some Coq developers
+   maintain a working version as Coq development goes at the
+   coq-contrib project on INRIA's GForge [1] (in Saclay directory).
+
+   [1] http://gforge.inria.fr/projects/coq-contribs/
+
+
+Patching upstream sources
+-------------------------
+
+This source package uses quilt to apply and remove its patches. Please
+refer to `/usr/share/doc/quilt/README.source' for information about
+how to use quilt for source packages.
+
+The quilt series is generated from the Git repository, using
+dom-{apply,save}-patches, from the dh-ocaml (>= 0.5) package. Please
+refer to the appendix about Git in the Debian OCaml Packaging Policy
+(from the same package).
+
+
+Building arch:all package
+-------------------------
+
+Building the arch:all package, libssreflect-coq, is not supported on
+architectures with native compiler, but with no natdynlink (only armel
+at the time of writing).
+
+ -- Stéphane Glondu <glondu@debian.org>, Sun, 24 Apr 2011 14:29:19 +0200
diff --git a/debian/changelog b/debian/changelog
new file mode 100644
index 0000000..7c3dbbe
--- /dev/null
+++ b/debian/changelog
@@ -0,0 +1,273 @@
+ssreflect (1.11.0-1) unstable; urgency=medium
+
+  * New upstream release
+  * Debhelper compatibility level 13:
+    -drop override of dh_missing which is no longer needed
+  * Set Rules-Requires-Root to no
+
+ -- Ralf Treinen <treinen@debian.org>  Fri, 11 Sep 2020 08:32:09 +0200
+
+ssreflect (1.10.0+dfsg-2) unstable; urgency=medium
+
+  * Rebuild against coq 8.11.0
+  * Standards-version 4.5.0 (no change)
+
+ -- Ralf Treinen <treinen@debian.org>  Fri, 06 Mar 2020 21:43:51 +0100
+
+ssreflect (1.10.0+dfsg-1) unstable; urgency=medium
+
+  * New upstream release
+  * gbp.conf: update import filter
+  * debian/rules: explicit targets to make: all, doc
+  * debian/libssreflect-coq.docs: doc now built in mathcomp/_build_doc/htmldoc/
+  * Add lintian-overrides for doc files whose filenames contain wildcards
+  * Standards-Version 4.4.1 (no change)
+  * Add build-dependency on lua
+
+ -- Ralf Treinen <treinen@debian.org>  Thu, 05 Dec 2019 23:06:05 +0100
+
+ssreflect (1.9.0+dfsg-2) unstable; urgency=medium
+
+  * Recompile with OCaml 4.08.1
+
+ -- Stéphane Glondu <glondu@debian.org>  Fri, 15 Nov 2019 10:26:00 +0100
+
+ssreflect (1.9.0+dfsg-1) unstable; urgency=medium
+
+  * New upstream release.
+    Repack upstream (remove docs/htmldoc/js/ and docs/javascripts/).
+  * Build-depends: minimal coq version 8.7, according to opam file.
+  * Standards-Version 4.4.0 (no change)
+  * debian/libssreflect-coq.docs: ChangeLog => CHANGELOG.md
+
+ -- Ralf Treinen <treinen@debian.org>  Tue, 20 Aug 2019 09:47:51 +0200
+
+ssreflect (1.7.0+dfsg-1) unstable; urgency=medium
+
+  * New upstream version. This fixes a FTBFS with coq 8.9.0 (closes: #919461)
+    Repack upstream (remove docs/htmldoc/js/)
+  * Update debian/watch to github
+  * Update Vcs-* to salsa
+  * Standards-Version 4.3.0
+    - https in format string of debian/copyright
+  * d/rules: fix installation of htmldocs
+  * Drop packages libssreflect-ocaml[-dev] as the plugin is now included in
+    the coq package.
+  * d/libssreflect-coq.docs: adjust pathnames of files
+  * d/copyright: drop short paragraph at first occurrence of CeCILL-B
+  * Build-depend on debhelper-compat (=12)
+    - use dh_missing (instead of dh_install) with --fail-missing
+  * No more compilation with ocaml:
+    - dropped build-dependencies on ocaml stuff
+    - dropped --with-ocaml flag to dh and usage of ocamlvars.mk
+  * Updated short and long description. Thanks to Enrico Tassi.
+  * Added an as-installed test, thanks again to Enrico Tassi.
+  * Added myself as Uploader.
+
+ -- Ralf Treinen <treinen@debian.org>  Sat, 16 Feb 2019 20:06:49 +0100
+
+ssreflect (1.6.1-3) unstable; urgency=medium
+
+  * Recompile with OCaml 4.05.0
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 09 Oct 2017 10:43:03 +0200
+
+ssreflect (1.6.1-2) unstable; urgency=medium
+
+  * Fix build-arch target
+
+ -- Enrico Tassi <gareuselesinge@debian.org>  Fri, 30 Dec 2016 11:39:11 +0100
+
+ssreflect (1.6.1-1) unstable; urgency=medium
+
+  * New upstream release
+
+ -- Enrico Tassi <gareuselesinge@debian.org>  Tue, 27 Dec 2016 16:10:53 +0000
+
+ssreflect (1.6-1) unstable; urgency=medium
+
+  * Adding myself as co-maintainer.
+  * Update upstream version to 1.6
+
+ -- Enrico Tassi <gareuselesinge@debian.org>  Tue, 30 Aug 2016 16:02:06 +0200
+
+ssreflect (1.5-3) unstable; urgency=medium
+
+  * Recompile with OCaml 4.02.3
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 14 Oct 2015 11:42:57 +0200
+
+ssreflect (1.5-2) unstable; urgency=medium
+
+  * Recompile with coq 8.4pl4
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 30 Jul 2014 10:21:09 +0200
+
+ssreflect (1.5-1) unstable; urgency=medium
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 13 Mar 2014 13:25:52 +0100
+
+ssreflect (1.5~rc1-3) unstable; urgency=medium
+
+  * Recompile with coq 8.4pl3
+  * Bump Standards-Version to 3.9.5 (no changes)
+  * Update debian/watch
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 20 Jan 2014 08:53:40 +0100
+
+ssreflect (1.5~rc1-2) unstable; urgency=low
+
+  * Upload to unstable
+  * Update Homepage
+
+ -- Stéphane Glondu <glondu@debian.org>  Fri, 06 Dec 2013 08:28:06 +0100
+
+ssreflect (1.5~rc1-1) experimental; urgency=low
+
+  * New upstream release
+  * Update Vcs-*
+  * Compile with OCaml >= 4
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 10 Aug 2013 22:11:00 +0200
+
+ssreflect (1.4-2) unstable; urgency=low
+
+  * Bump debhelper compat level to 8
+  * Bump Standards-Version to 3.9.4
+  * Upload to unstable
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 09 May 2013 13:36:48 +0200
+
+ssreflect (1.4-1) experimental; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 18 Sep 2012 16:45:50 +0200
+
+ssreflect (1.3pl4-1) unstable; urgency=low
+
+  * New upstream release
+  * Put debian/copyright in format 1.0
+  * Bump Standards-Version to 3.9.3
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 09 Jun 2012 09:35:40 +0200
+
+ssreflect (1.3pl2-4) unstable; urgency=medium
+
+  * Fix compilation with camlp5 6.05 and coq 8.3pl4
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 01 Apr 2012 16:43:46 +0200
+
+ssreflect (1.3pl2-3) unstable; urgency=low
+
+  * Recompile with camlp5 6.04 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 06 Mar 2012 08:29:13 +0100
+
+ssreflect (1.3pl2-2) unstable; urgency=low
+
+  * Rebuild with Coq 8.3pl3
+    - cherry-pick patch from coq-contrib to fix FTBFS with Coq 8.3pl3
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 25 Dec 2011 17:28:19 +0100
+
+ssreflect (1.3pl2-1) unstable; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 22 Nov 2011 07:16:04 +0100
+
+ssreflect (1.3pl1-5) unstable; urgency=low
+
+  * Recompile with OCaml 3.12.1 (no changes)
+  * Bump Standards-Version to 3.9.2 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 03 Nov 2011 06:30:00 +0100
+
+ssreflect (1.3pl1-4) unstable; urgency=low
+
+  * Build theories only when explicitly asked (fixes FTBFS on armel as
+    a side-effect)
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 24 Apr 2011 14:44:33 +0200
+
+ssreflect (1.3pl1-3) unstable; urgency=low
+
+  * Upload to unstable
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 21 Apr 2011 13:59:00 +0200
+
+ssreflect (1.3pl1-1) experimental; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 31 Mar 2011 10:52:00 +0200
+
+ssreflect (1.3-1) experimental; urgency=low
+
+  * New upstream release, compatible with Coq 8.3:
+    - remove 0001-Build-as-a-plugin.patch
+    - add 0001-Fix-tests-Make.patch
+    - this version is under CeCILL-B only; update debian/copyright
+      accordingly
+  * Bump Standards-Version to 3.9.1 (no changes)
+  * Update debian/watch
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 15 Mar 2011 08:47:47 +0100
+
+ssreflect (1.2+dfsg-7) unstable; urgency=low
+
+  * Rebuild against camlp5 6.02.1
+  * Bump versioned build-dependency to libcoq-ocaml-dev to ease camlp5
+    transition
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 22 Feb 2011 11:22:15 +0100
+
+ssreflect (1.2+dfsg-6) unstable; urgency=low
+
+  * Rebuild against OCaml 3.11.2
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 15 Jul 2010 13:41:07 +0200
+
+ssreflect (1.2+dfsg-5) unstable; urgency=low
+
+  * Rebuild with Coq 8.2pl2
+  * debian/control:
+    - replace Conflicts by Breaks
+    - bump Standards-Version to 3.9.0
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 14 Jul 2010 15:19:10 +0200
+
+ssreflect (1.2+dfsg-4) unstable; urgency=low
+
+  * Rebuild with OCaml 3.11.2
+  * Bump Standards-Version to 3.8.4 (no changes)
+  * Update watch file
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 11 Feb 2010 10:30:30 +0100
+
+ssreflect (1.2+dfsg-3) unstable; urgency=low
+
+  * debian/control:
+    - add libssreflect-ocaml-dev binary package
+    - put *ocaml* packages in ocaml section
+    - libssreflect-ocaml enhances coq
+  * Switch to dh-ocaml 0.9
+  * Switch to format 3.0 (quilt)
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 19 Dec 2009 17:30:57 +0100
+
+ssreflect (1.2+dfsg-2) unstable; urgency=low
+
+  * Use -R when invoking coq_makefile to avoid warnings and need of
+    explicit exclusion of ssreflect path; set it to user-contrib/Ssreflect
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 02 Sep 2009 19:18:26 +0200
+
+ssreflect (1.2+dfsg-1) unstable; urgency=low
+
+  * Initial release (Closes: #508468)
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 26 Aug 2009 23:41:27 +0200
diff --git a/debian/control b/debian/control
new file mode 100644
index 0000000..db9364a
--- /dev/null
+++ b/debian/control
@@ -0,0 +1,42 @@
+Source: ssreflect
+Priority: optional
+Maintainer: Debian OCaml Maintainers <debian-ocaml-maint@lists.debian.org>
+Uploaders: Stéphane Glondu <glondu@debian.org>,
+ Enrico Tassi <gareuselesinge@debian.org>,
+ Ralf Treinen <treinen@debian.org>
+Build-Depends:
+ debhelper-compat (= 13),
+ coq (>= 8.7),
+ lua5.1
+Rules-Requires-Root: no
+Standards-Version: 4.5.0
+Section: math
+Homepage: https://math-comp.github.io/math-comp/
+Vcs-Browser: https://salsa.debian.org/ocaml-team/ssreflect
+Vcs-Git: https://salsa.debian.org/ocaml-team/ssreflect.git
+
+Package: libssreflect-coq
+Architecture: all
+Depends:
+ libcoq-ocaml,
+ coq-${F:CoqABI},
+ ${misc:Depends}
+Provides: ssreflect, libmathcomp-coq
+Description: Mathematical Components library for Coq
+ The Mathematical Components Library is an extensive and coherent
+ repository of formalized mathematical theories. It is based on the
+ Coq proof assistant, powered with the Coq/SSReflect language.
+ .
+ These formal theories cover a wide spectrum of topics, ranging from
+ the formal theory of general-purpose data structures like lists,
+ prime numbers or finite graphs, to advanced topics in algebra.
+ .
+ The formalization technique adopted in the library, called "small
+ scale reflection", leverages the higher-order nature of Coq's
+ underlying logic to provide effective automation for many small,
+ clerical proof steps. This is often accomplished by restating
+ ("reflecting") problems in a more concrete form, hence the name. For
+ example, arithmetic comparison is not an abstract predicate, but
+ rather a function computing a Boolean.
+ .
+ This package installs the full Mathematical Components library.
diff --git a/debian/copyright b/debian/copyright
new file mode 100644
index 0000000..9c36253
--- /dev/null
+++ b/debian/copyright
@@ -0,0 +1,595 @@
+Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+Packaged-By: Stéphane Glondu <glondu@debian.org>
+Packaged-Date: Wed, 26 Aug 2009 13:17:54 +0200
+Original-Source-Location: http://www.msr-inria.inria.fr/Projects/math-components
+Upstream-Author:
+  Andrea Asperti,
+  Jeremy Avigad
+  Yves Bertot,
+  Cyril Cohen,
+  François Garillot,
+  Georges Gonthier,
+  Stéphane Le Roux,
+  Assia Mahboubi,
+  Sidi Ould Biha,
+  Ioana Pasca,
+  Laurence Rideau,
+  Enrico Tassi,
+  Laurent Théry
+
+Files: *
+Copyright: © 2005-2011 Microsoft Corporation and INRIA
+License: CeCILL-B
+
+Files: debian/*
+Copyright: © 2008-2011 Stéphane Glondu <glondu@debian.org>
+License: CeCILL-B
+
+Files: htmldoc/js/dagre.js
+Copyright: © 2012-2014 Chris Pettitt <cpettitt@gmail.com>
+License: Expat
+
+Files: htmldoc/js/cytoscape*.js
+Copyright: © 2016 The Cytoscape Consortium
+License: LGPL-3+
+ This package is free software; you can redistribute it and/or
+ modify it under the terms of the GNU Lesser General Public
+ License as published by the Free Software Foundation; either
+ version 3 of the License, or (at your option) any later version.
+ .
+ This package is distributed in the hope that it will be useful,
+ but WITHOUT ANY WARRANTY; without even the implied warranty of
+ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
+ Lesser General Public License for more details.
+ .
+ You should have received a copy of the GNU General Public License
+ along with this program. If not, see <http://www.gnu.org/licenses/>.
+ .
+ On Debian systems, the complete text of the GNU Lesser General
+ Public License can be found in "/usr/share/common-licenses/LGPL-3".
+
+Files: htmldoc/js/jquery-2.0.3.js
+Copyright: 2005, 2013 jQuery Foundation, Inc. and other contributors
+License: Expat
+
+Files: htmldoc/js/jquery-qtip.js
+Copyright: 2013 Craig Michael Thompson
+License: Expat or GPL
+
+License: GPL
+ Unspecified GPL version
+
+License: Expat
+ Permission is hereby granted, free of charge, to any person obtaining a copy of
+ this software and associated documentation files (the "Software"), to deal in
+ the Software without restriction, including without limitation the rights to
+ use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
+ of the Software, and to permit persons to whom the Software is furnished to do
+ so, subject to the following conditions:
+ .
+ The above copyright notice and this permission notice shall be included in all
+ copies or substantial portions of the Software.
+ .
+ THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+ SOFTWARE.
+
+License: CeCILL-B
+ 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/debian/gbp.conf b/debian/gbp.conf
new file mode 100644
index 0000000..4fc6b3c
--- /dev/null
+++ b/debian/gbp.conf
@@ -0,0 +1,7 @@
+[DEFAULT]
+pristine-tar = True
+
+[import-orig]
+filter = [
+       'docs/htmldoc/js/*',
+       'docs/javascripts/*' ]
diff --git a/debian/libssreflect-coq.README.Debian b/debian/libssreflect-coq.README.Debian
new file mode 100644
index 0000000..224010c
--- /dev/null
+++ b/debian/libssreflect-coq.README.Debian
@@ -0,0 +1,11 @@
+Ssreflect for Debian
+====================
+
+This package doesn't provide the ssrcoq binary as built originally by
+upstream (but relies on dynamic linking instead), nor the PDF
+documentation (which is available online, see README).
+
+You can use Ssreflect directly with the regular Coq tools. For
+compatibility, a symlink to coqtop named "ssrcoq" is provided.
+
+ -- Stéphane Glondu <glondu@debian.org>, Tue,  1 Sep 2009 15:08:28 +0200
diff --git a/debian/libssreflect-coq.doc-base b/debian/libssreflect-coq.doc-base
new file mode 100644
index 0000000..4199932
--- /dev/null
+++ b/debian/libssreflect-coq.doc-base
@@ -0,0 +1,9 @@
+Document: mathematical-components-library
+Title: The Mathematical Components Library
+Author: The Mathematical Components Development Team
+Abstract: This is the coqdoc-generated documentation for Mathematical Components
+Section: Science/Mathematics
+
+Format: HTML
+Index: /usr/share/doc/libssreflect-coq/htmldoc/index.html
+Files: /usr/share/doc/libssreflect-coq/htmldoc/*.html
diff --git a/debian/libssreflect-coq.docs b/debian/libssreflect-coq.docs
new file mode 100644
index 0000000..f1da7e0
--- /dev/null
+++ b/debian/libssreflect-coq.docs
@@ -0,0 +1,3 @@
+CHANGELOG.md
+README.md
+mathcomp/_build_doc/htmldoc/
diff --git a/debian/libssreflect-coq.examples b/debian/libssreflect-coq.examples
new file mode 100644
index 0000000..6b59762
--- /dev/null
+++ b/debian/libssreflect-coq.examples
@@ -0,0 +1 @@
+mathcomp/ssreflect/pg-ssr.el
diff --git a/debian/libssreflect-coq.install b/debian/libssreflect-coq.install
new file mode 100644
index 0000000..467fefe
--- /dev/null
+++ b/debian/libssreflect-coq.install
@@ -0,0 +1,3 @@
+usr/lib/coq/user-contrib/mathcomp/*/*.vo
+usr/lib/coq/user-contrib/mathcomp/*/*.v
+usr/lib/coq/user-contrib/mathcomp/*/*.glob
diff --git a/debian/libssreflect-coq.lintian-overrides b/debian/libssreflect-coq.lintian-overrides
new file mode 100644
index 0000000..9d8c022
--- /dev/null
+++ b/debian/libssreflect-coq.lintian-overrides
@@ -0,0 +1,14 @@
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_abbreviation_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_axiom_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_constructor_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_definition_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_global_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_inductive_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_lemma_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_library_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_module_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_notation_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_projection_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_record_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_section_*.html
+libssreflect-coq: file-name-contains-wildcard-character usr/share/doc/libssreflect-coq/htmldoc/index_variable_*.html
diff --git a/debian/rules b/debian/rules
new file mode 100755
index 0000000..498653d
--- /dev/null
+++ b/debian/rules
@@ -0,0 +1,22 @@
+#!/usr/bin/make -f
+
+include /usr/share/coq/coqvars.mk
+
+export COQTOP := $(COQ_STDLIB_DIR)
+export COQLIB := $(COQ_STDLIB_DIR)
+export COQBIN := /usr/bin/
+
+%:
+	dh $@
+
+.PHONY: override_dh_auto_build
+override_dh_auto_build:
+	$(MAKE) -C mathcomp all doc
+
+.PHONY: override_dh_auto_install
+override_dh_auto_install:
+	$(MAKE) -C mathcomp install DSTROOT=$(CURDIR)/debian/tmp
+
+.PHONY: override_dh_gencontrol
+override_dh_gencontrol:
+	dh_gencontrol -- -VF:CoqABI="$(COQ_ABI)"
diff --git a/debian/source/format b/debian/source/format
new file mode 100644
index 0000000..46ebe02
--- /dev/null
+++ b/debian/source/format
@@ -0,0 +1 @@
+3.0 (quilt)
\ No newline at end of file
diff --git a/debian/tests/control b/debian/tests/control
new file mode 100644
index 0000000..0ec7c8c
--- /dev/null
+++ b/debian/tests/control
@@ -0,0 +1,2 @@
+Tests: loadssreflect
+Depends: @, coq
diff --git a/debian/tests/loadssreflect b/debian/tests/loadssreflect
new file mode 100755
index 0000000..f172975
--- /dev/null
+++ b/debian/tests/loadssreflect
@@ -0,0 +1,11 @@
+#!/bin/sh
+
+set -e
+
+outdir=${ADT_ARTIFACTS-/tmp/ssreflect}
+indir="debian/tests"
+input="loadssreflect.v"
+mkdir -p ${outdir}
+cp ${indir}/${input} ${outdir}
+cd ${outdir}
+coqc ${input} 2> /dev/null
diff --git a/debian/tests/loadssreflect.v b/debian/tests/loadssreflect.v
new file mode 100644
index 0000000..4ce3dd3
--- /dev/null
+++ b/debian/tests/loadssreflect.v
@@ -0,0 +1 @@
+From mathcomp Require Import all_ssreflect.
diff --git a/debian/watch b/debian/watch
new file mode 100644
index 0000000..faf119b
--- /dev/null
+++ b/debian/watch
@@ -0,0 +1,3 @@
+version=3
+opts=uversionmangle=s/(\d)(rc\d*)$/$1~$2/,dversionmangle=s/\+dfsg$// \
+https://github.com/math-comp/math-comp/releases .*/mathcomp-([0-9.]*).tar\.gz