.gitignore

-.pc

.travis.yml

+dist: trusty
+sudo: required
+language: c
+cache:
+  apt: true
+  directories:
+  - $HOME/.opam
+addons:
+  apt:
+    sources:
+    - avsm
+    packages:
+    - opam
+    - aspcud
+env:
+  global:
+  - NJOBS=2
+  # system is == 4.02.3
+  - COMPILER="system"
+  # Main test targets
+  matrix:
+  - TEST_TARGET="v8.6"
+  - TEST_TARGET="v8.7"
+  - TEST_TARGET="v8.8"
+  - TEST_TARGET="master"
+
+install:
+- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y
+- eval $(opam config env)
+- opam config var root
+- opam install -j ${NJOBS} -y ocamlfind camlp5 ${EXTRA_OPAM}
+- opam list
+- git clone --depth 1 -b ${TEST_TARGET} https://github.com/coq/coq.git coq-${TEST_TARGET}
+- cd coq-${TEST_TARGET}
+- ./configure -native-compiler no -local -coqide no
+- make -j ${NJOBS}
+- cd -
+
+script:
+- echo 'Building Mathcomp...' && echo -en 'travis_fold:start:mathcomp.build\\r'
+- export PATH=`pwd`/coq-${TEST_TARGET}/bin:$PATH
+- cd mathcomp
+- make Makefile.coq
+- make -f Makefile.coq -j ${NJOBS} all
+- echo -en 'travis_fold:end:mathcomp.build\\r'

CONTRIBUTING.md

+# Contribution Guide for the Mathematical Components library
+
+We describe here best practices for contributing to the library. In
+particular we explain what conventions are used in the library. When
+contributing, you should comply to these conventions to get your code
+integrated to the library.
+
+This file is not comprehensive yet and might still contain mistakes or
+unclear indications, please consider contributing.
+
+## Proof style.
+### General guidelines
+- **A line should have no more than 80 characters**. If a line is
+longer than that, it should be cut semantically. If there is no way to
+make a semantic cut (e.g. the user provides an explicit term that is
+too long to fit on one line), then just cut it over several lines to
+make it readable.
+- Lines end with a point `.` and only have `;` inside them.
+- Lines that close a goal must start with a terminator (`by` or
+  `exact`). You should consider using an editor that highlight those
+  terminators in a specific color (e.g. red).
+
+### Spaces
+We write
+- `move=>` and `move:` (no space between `move` and `=>` or `:`)
+- `apply/` and `apply:` (no space between `apply` and `/` or `:`)
+- `rewrite /definition` (there is a space between `rewrite` and an unfold)
+
+### Indentation in proof scripts
+- When two subgoals are created, the first subgoal is indented by 2
+  spaces, the second is not. Use `last first` to bring the
+  smallest/less meaningful goal first, and keep the main flow of the
+  proof unindented.
+- When more than two subgoals are created, bullets are used `-` for
+  the first level, `+` for the second and `*` for the third as in:
+  ```
+  tactic.
+  - tactic.
+    + tactic.
+      * tactic.
+      * tactic.
+      * tactic.
+    + tactic.
+    + tactic.
+  - tactic
+  - tactic
+  ```
+
+  If all the subgoals have the same importance, use bullets for all of
+  them, however, if one goal is more important than the others
+  (i.e. is main flow of the proof). Then you might remove the bullet
+  for this last one and unindent it as in:
+  ```
+  tactic.
+  - tactic. (* secondary subgoal 1 *)
+  - tactic. (* secondary subgoal 2 *)
+  tactic. (* third subgoal is the main one *)
+  ```
+
+## Statements of lemmas, theorems and definitions.
+
+- Universal quantifications with dependent variable should appear on the left hand side of the colon, until we reach the first non dependent variables. e.g.
+  `Lemma example x y : x < y -> x >= y = false`
+
+### Term style.
+- Operators are surrounded by space, for example `n*m` should be written `n * m`.
+This particular example can be problematic if matrix.v is imported because then, `M *m N` is matrix product.
+
+### Naming of variables
+- Variable names follow the following conventions.
+  + Hypothesis should not be named `H`, `H'`,... (these collide with
+  subgroup variable conventions) but have meaningful names. For
+  example, an hypothesis `n > 0` should be named `n_gt0`.
+  + Induction Hypotheses are prefixed by `IH` or `ih` (e.g. induction hypothesis on `n` is called `IH`).
+  + Natural numbers and integers should be named `m`, `n`, `p`, `d`, ...
+  + Elements of another ring should be named `x`, `y`, `z`, `u`, `v`, `w`, ...
+  + Polynomials should be named by lower case letter `p`, `q`, `r` ... (to avoid collision with properties named `P`, `Q`, ...)
+  + Matrices should be named `A`, `B`, ..., `M`, `N`, ...

ChangeLog

-21/12/2016 - point release to support Coq 8.6 - version 1.6.1
-	* ssreflect/plugin/v8.6: port of the plugin to Coq 8.6
-	* ssreflect/plugin/: bug fixes (most apply only on Coq 8.5 and 8.6):
-	    - rewrite /primitive_projection not working (#85)
-	    - ssrpatternarg parsed with no brackets
-	    - rewrite does not instantiate evars in goals (regression since 8.4)
-	    - SsrHave NoTCResolution plays well with undo (#6)
-	    - Type Classes resolution performed in the correct set of universe 
-	      constraints (#22)
-	    - Do not hide critical errors with a blind catch all (#19)
-	    - Explicit error message if rewrite fails due to Type Classes
-	      resolution (#21, also for Coq 8.4)
-	    - elim/v handles eliminator from Derive Inversion (#2)
+24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
+
+	* Added compatibility with Coq 8.8 and lost compatibility with
+	  Coq <= 8.5. This release is compatible with Coq 8.6, 8.7 and 8.8.
+
+	* Integration to Coq: ssrbool.v ssrfun.v and plugin.
+	  ssrtest also moved to Coq test suite.
+
+	* Cleaning up the github repository: the math-comp repository is
+	  now dedicated to the released material (as in the present
+	  release). For instance, directories real-closed and odd-order now
+	  have their own repository.
+
+	* Library refactoring: algC ssrnum: Library ssrnum.v now
+	  provides an interface numClosedFieldType, which abstracts the
+	  theory of algebraic numbers. In particular, Re, Im, 'i,
+	  conjC, n.-root and sqrtC, previously defined in library algC.v,
+	  are now part of this generic interface. In case of ambiguity,
+	  a cast to type algC, of complex algebraic numbers, can be used to
+	  disambiguate via  typing constraints. Some theory was thus made
+	  more generic, and the corresponding lemmas, previously defined in
+	  library algC.v (e.g. conjCK) now feature an extra, non maximal
+	  implicit, parameter of type numClosedFieldType. This could break
+	  some proofs.
+
+	* Lemma dvdn_fact was moved from library prime.v to library div.v
+
+	* Structures, changes in interfaces:
+	  numClosedFieldType
+
+	* New Theorems:
+	  iter_in, finv_in, inv_f_in, finv_inj_in, fconnect_sym_in,
+	  iter_order_in, iter_finv_in, cycle_orbit_in, fpath_finv_in,
+	  fpath_finv_f_in, fpath_f_finv_in
+	  big_allpairs
+	  uniqP, uniqPn
+	  dec_factor_theorem,
+	  mul_bin_down, mul_bin_left
+          abstract_context (now merged in Coq)
+
+	* Renamed/generalized:
+	  mul_Sm_binm -> mul_bin_diag
+	  divn1 -> divz1 (in intdiv)
+	  rootC -> nthroot
+	  algRe -> Re
+	  algIm -> Im
+	  algCi -> imaginaryC
+  	  reshape_index_leq -> reshape_leq
+	  Every theorem from ssrnum that used to be in algC
+
+	* Generalized or improved:
+	  ltngtP, contra_eq, contra_neq, odd_opp, nth_iota
 
 24/11/2015 - major reorganization of the archive - version 1.6
-	* Files split into subdirectories: ssreflect, algebra, fingroup,
+
+	* Files split into sub-directories: ssreflect, algebra, fingroup,
 	  solvable, field and character. In this way the user can decide
 	  to compile only the subset of the Mathematical Components library
 	  that is relevant to her. Note that this introduces a possible
@@ -28,7 +68,7 @@
 		https://github.com/math-comp/ssr-manual
 	  Pull requests improving the documentation are welcome.
 
-	* Renamings or replacements:
+	* Renaming or replacements:
 	  conjC_closed -> cfConjC_closed
 	  class_transr -> class_eqP
 	  cfclass_transl -> cfclass_transr

INSTALL

-# INSTALLATION PROCEDURE
-
-Users familiar with OPAM can use such tool to install Coq and the Mathematical Components library with commands like
-`opam coq-mathcomp-fingroup`.
-
-This document is for users that installed Coq in another way, for example
-compiling it from sources.
-
-## REQUIREMENTS
-
-Coq version 8.4pl6 or 8.5 (at the time of writing, beta3)
-
-## BUILDING
-
-The Mathematical Components library is divided into various installation
-units.  On can install the entire library (compilation time is around 35 minutes) or only some of its units.
-
-In both cases, if Coq is not installed such that its binaries like `coqc`
-and `coq_makefile` are in the PATH, then the COQBIN environment variable
-must be set to point to the directory containing such binaries.
-For example:
-
-    export COQBIN=/home/user/coq/bin/
-
-Now, to install the entire library, including the SSReflect proof language:
-
-    cd mathcomp-1.6/mathcomp
-    make -j2 && make install
-
-If one wants to only install a few modules he should instead run make
-inside the modules he wants to install *in the following order*:
-
-  1. ssreflect
-  2. fingroup
-  3. algebra
-  4. solvable
-  5. field
-  6. character
-
-This means that one cannot install, say, algebra without having already
-installed fingroup. An example:
-
-    cd mathcomp-1.6/mathcomp
-    cd ssreflect && make -j2 && make install
-    cd ../fingroup && make -j2 && make install
-
-## CUSTOMIZATION OF THE PROOF GENERAL EMACS INTERFACE
-
-The `mathcomp/ssreflect/` directory comes with a small configuration file
-`pg-ssr.el` to extend ProofGeneral (PG), a generic interface for
-proof assistants based on the customizable text editor Emacs, to the
-syntax of ssreflect.
-
-The >= 3.7 versions of ProofGeneral support this extension.
-
-- Following the installation instructions, unpack the sources of PG in
-a directory, for instance <my-pgssr-location>/ProofGeneral-3.7, and add
-the following line to your .emacs file.
-Under Unix/MacOS:
-
-    (load-file
-      "<my-pg-location>/ProofGeneral-3.7/generic/proof-site.el" )
-    (load-file "<my-pgssr-location>/pg-ssr.el")
-
-Under Windows+Cygwin:
-
-    (load-file
-      "C:\\<my-pg-location>\\ProofGeneral-3.7\\generic\\proof-site.el")
-    (load-file "<my-pgssr-location>\\pg-ssr.el")
-
-Where <my-pg-location> is the location of your own ProofGeneral
-directory, and where <my-pgssr-location> is the location of your pg-ssr.el
-file.
-
-Coq sources have a .v extension. Opening any .v file should
-automatically launch ProofGeneral.
-
-## TRANSITION FROM 1.5 to 1.6
-
-The change of logical/physical paths implied by the reorganization of the
-library causes an incompatibility for users of previous version of the
-Mathematical Components library. For instance the command line
-
-          Require Ssreflect.ssreflect.
-
-does not work anymore.  We propose a replacement schema for such
-command lines that is compatible with both versions 8.4 and 8.5 of
-Coq, namely replacing the previous line with:
-
-          Require Import mathcomp.ssreflect.ssreflect.
-
-          From mathcomp Require Import ssrfun ssrbool ...
-
-The first line loads the ssreflect plugin using its full path.
-Then all other files are loaded from the mathcomp name space.
-The component part (like ssreflect or algebra) is omitted.  All theory files in
-the library follow this schema.
-Note that the From directive has effect only in Coq 8.5. Coq 8.4 ignores it
-and searches for files in all known paths: hence beware of the
-possible name collisions.

INSTALL.md

+# Layout and compilation of the library
+
+The library is divided into packages which group together related
+files. Each package defines a distribution and compilation unit.
+
+Packages can be compiled using the traditional make utility or
+the more recent OPAM one. The released and current dev versions are
+also available as OPAM packages.
+
+## Compilation and installation of released and current dev version with OPAM
+If you just installed OPAM you may have to do the following. You may also want
+to read [OPAM user manual](https://opam.ocaml.org/doc/Usage.html) first. 
+```
+opam init
+eval `opam config env`
+```
+Once your OPAM environment is configured
+you can install any math-comp package via
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam pin add -n coq -k version 8.8.0
+opam install coq -j3
+opam install coq-mathcomp-ssreflect.1.7.0 -j3
+```
+Replace `ssreflect` here by the package you want, the dependencies will be
+installed automatically. We recommend pinning a particular version of Coq
+(here `8.8.0`).
+To get the latest development version you need to execute the following:
+```
+opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
+opam install coq-mathcomp-ssreflect.dev -j3
+```
+
+## Compilation and installation with make
+
+The instructions assume you are in the `mathcomp` directory and that
+you have a supported version of Coq: 8.6, 8.7 or 8.8.
+
+If `coqc` is in your `PATH`, then you are good to go.  Alternatively, you
+can export the `COQBIN` variable to tell `make` where the `coqc` binary is:
+```
+export COQBIN=/home/gares/COQ/coq/bin/
+```
+
+To compile the entire library just type `make`. If you have parallel
+hardware then `make -j 3` is probably a faster option. 
+
+The files can be edited using CoqIDE or Proof General, or any
+other editor that understands the `_CoqProject` file, with no
+further configuration from the `mathcomp` directory.
+```
+coqide ssreflect/div.v
+```
+Note that you may need to enable `_CoqProject` processing in your
+editor (e.g. the default for CoqIDE is to ignore it).
+
+To install the compiled library, just execute `make install`.
+
+## Compilation and installation of a custom version using OPAM
+
+The instructions assume you are in the `mathcomp` directory
+and that you have OPAM installed and configured with the
+standard Coq repositories.
+
+For each package, pin the `opam` file:
+```
+opam pin -n add ssreflect
+```
+This can be achieved in one go as follows:
+```
+for P in */opam; do opam pin -n add ${P%%/opam}; done
+```
+
+Then you can use `opam install` to compile and install any package.
+For example:
+```
+opam install coq.8.8.0 coq-mathcomp-ssreflect
+```
+

README

-          THE MATHEMATICAL COMPONENTS LIBRARY
-       ------------------------------------------
-
-
-DOCUMENTATION
-=============
-
-	The documentation of the ssreflect tactics, a brief
-        description of the mathematical components libraries
-	and a detailed list of the changes made in the releases
-        is available as an Inria Research Report at
-
-        	http://hal.inria.fr/inria-00258384
-
-
-AVAILABILITY
-============
-
-	Ssreflect and the Mathematical Components library are available at:
-	http://math-comp.github.io/math-comp/
-
-
-THE DISCUSSION LIST
-===================
-
-	The ssreflect list (ssreflect@msr-inria.inria.fr) is meant to be
-        a standard way to discuss about the ssreflect extension and the
-        mathematical components library.
-
-	To subscribe visit: https://sympa.inria.fr/sympa/info/ssreflect
-
-LICENSING
-=========
-
-        This program is free software; you can redistribute it and/or modify
-        it under the terms of the CeCILL B FREE SOFTWARE LICENSE.
-
-        You should have received a copy of the CeCILL B License with this
-        Kit, in the file named "CeCILL-B".
-        If not, visit http://www.cecill.info

README.md

+[![Build Status](https://travis-ci.org/math-comp/math-comp.svg?branch=master)](https://travis-ci.org/math-comp/math-comp)
+
+# The Mathematical Components repository
+
+The Mathematical Components Library is an extensive and coherent
+repository of formalized mathematical theories. It is based on
+the [Coq](http://coq.inria.fr) proof assistant, powered with the
+[Coq/SSReflect](https://coq.inria.fr/distrib/current/refman/ssreflect.html)
+language.
+
+These formal theories cover a wide spectrum of topics, ranging from the formal theory of general purpose data structures like [lists](mathcomp/ssreflect/seq.v), [prime numbers](mathcomp/ssreflect/prime.v) or [finite graphs](mathcomp/ssreflect/fingraph.v), to advanced topics in algebra. The repository includes the foundation of formal theories used in a [formal proof](https://www.ams.org/notices/200811/tx081101382p.pdf) of the [Four Colour Theorem](https://en.wikipedia.org/wiki/Four_color_theorem) (Appel - Haken, 1976) and a [mechanization](https://hal.archives-ouvertes.fr/hal-00816699/) of the [Odd Order Theorem](https://en.wikipedia.org/wiki/Feit%E2%80%93Thompson_theorem) (Feit - Thompson, 1963), a landmark result of finite group theory, which utilizes the library extensively.
+
+## Installation
+
+If you already have OPAM installed:
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released
+opam install coq-mathcomp-ssreflect
+```
+
+Additional packages go by the name of `coq-mathcomp-algebra`,
+`coq-mathcomp-field`, etc... See [INSTALL](INSTALL.md) for detailed
+installation instructions in other scenarios.
+
+## How to get help
+
+- The [ssreflect mailing
+  list](https://sympa.inria.fr/sympa/info/ssreflect) is the primary
+  venue for help and questions about the library.
+- The [Mathematical Components Book](https://math-comp.github.io/mcb/)
+  provides a comprehensive introduction to the library.
+- The [MathComp wiki](https://github.com/math-comp/math-comp/wiki)
+  contains many useful information, including including a list of
+  [tutorials](https://github.com/math-comp/math-comp/wiki/tutorials).
+- Experienced users hang around at
+  [StackOverflow](https://stackoverflow.com/questions/tagged/ssreflect)
+  listening to the `ssreflect` and `coq` tags.
+
+## Publications and Tools using MathComp
+
+A collection of [papers](https://github.com/math-comp/math-comp/wiki/Publications) 
+using the Mathematical Components library can be found on the
+[wiki](https://github.com/math-comp/math-comp/wiki).

debian/changelog

+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

debian/compat

-8

debian/control

 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>
+Uploaders: Stéphane Glondu <glondu@debian.org>,
+ Enrico Tassi <gareuselesinge@debian.org>,
+ Ralf Treinen <treinen@debian.org>
 Build-Depends:
- debhelper (>= 8),
- coq (>= 8.6),
- libcoq-ocaml-dev (>= 8.4),
- dh-ocaml (>= 0.9~),
- camlp5 (>= 5.12-2~),
- ocaml-best-compilers,
- ocaml-nox (>= 4)
-Standards-Version: 3.9.5
+ debhelper-compat (= 12),
+ coq (>= 8.6)
+Standards-Version: 4.3.0
 Section: math
 Homepage: https://math-comp.github.io/math-comp/
-Vcs-Browser: http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/ssreflect.git
-Vcs-Git: git://anonscm.debian.org/pkg-ocaml-maint/packages/ssreflect.git
-
-Package: libssreflect-ocaml
-Section: ocaml
-Architecture: any
-Depends:
- ${ocaml:Depends},
- ${shlibs:Depends},
- ${misc:Depends}
-Enhances: coq
-Provides: ${ocaml:Provides}
-Description: small scale reflection extension for Coq (plugin)
- This package is part of Ssreflect, the small scale reflection
- extension for Coq. It provides a new tactic language, which promotes
- more structured, concise and robust proof scripts, and is in fact
- independent from the "reflection" proof style. It is implemented as a
- linkable extension to the Coq system.
-
-Package: libssreflect-ocaml-dev
-Section: ocaml
-Architecture: any
-Depends:
- ${ocaml:Depends},
- ${shlibs:Depends},
- ${misc:Depends}
-Replaces: libssreflect-ocaml (<< 1.2+dfsg-3~)
-Breaks: libssreflect-ocaml (<< 1.2+dfsg-3~)
-Provides: ${ocaml:Provides}
-Description: small scale reflection extension for Coq (devt files)
- This package is part of Ssreflect, the small scale reflection
- extension for Coq. It provides the static native-code library, needed
- to build custom toplevels, and the compiled interface.
+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:
- libssreflect-ocaml (>= ${source:Version}),
+ libcoq-ocaml,
  coq-${F:CoqABI},
  ${misc:Depends}
 Provides: ssreflect, libmathcomp-coq
-Description: small scale reflection library for Coq (theories)
- The name Ssreflect stands for "small scale reflection", a style of
- proof that evolved from the computer-checked proof of the Four Colour
- Theorem and which leverages the higher-order nature of Coq's
+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, in the Ssreflect library, arithmetic comparison is not an
- abstract predicate, but a function computing a boolean.
- .
- The Ssreflect distribution comprises two parts:
- * A new tactic language, which promotes more structured, concise and
-   robust proof scripts, and is in fact independent from the "reflection"
-   proof style. It is implemented as a linkable extension to the Coq
-   system.
- * A comprehensive set of Coq libraries covering topics as combinatorics
-   and algebra.
+ example, arithmetic comparison is not an abstract predicate, but
+ rather a function computing a Boolean.
  .
- This package installs the full Ssreflect distribution.
+ This package installs the full Mathematical Components library.

debian/copyright

-Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
+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
@@ -20,9 +20,6 @@ Upstream-Author:
 Files: *
 Copyright: © 2005-2011 Microsoft Corporation and INRIA
 License: CeCILL-B
- This program is free software; you can redistribute it and/or modify
- it under the terms of the CeCILL B FREE SOFTWARE LICENSE. The
- CeCILL-B full license is appended to this file.
 
 Files: debian/*
 Copyright: © 2008-2011 Stéphane Glondu <glondu@debian.org>

debian/libssreflect-coq.doc-base

@@ -5,5 +5,5 @@ Abstract: This is the coqdoc-generated documentation for Mathematical Components
 Section: Science/Mathematics
 
 Format: HTML
-Index: /usr/share/doc/libssreflect-coq/html/index.html
-Files: /usr/share/doc/libssreflect-coq/html/*.html
+Index: /usr/share/doc/libssreflect-coq/htmldoc/index.html
+Files: /usr/share/doc/libssreflect-coq/htmldoc/*.html

debian/libssreflect-coq.docs

-etc/ChangeLog
-etc/README
+ChangeLog
+README.md
+docs/htmldoc/
\ No newline at end of file

debian/libssreflect-coq.install

 usr/lib/coq/user-contrib/mathcomp/*/*.vo
 usr/lib/coq/user-contrib/mathcomp/*/*.v
 usr/lib/coq/user-contrib/mathcomp/*/*.glob
-html              usr/share/doc/libssreflect-coq

debian/libssreflect-ocaml-dev.install.in

-usr/lib/coq/user-contrib/mathcomp/ssreflect.cmi
-usr/lib/coq/user-contrib/mathcomp/ssreflect_plugin.cmi

debian/libssreflect-ocaml.install.in

-     usr/lib/coq/user-contrib/mathcomp/ssreflect_plugin.cmo
-DYN: usr/lib/coq/user-contrib/mathcomp/ssreflect_plugin.cmxs

debian/rules

 #!/usr/bin/make -f
 
 include /usr/share/coq/coqvars.mk
-include /usr/share/ocaml/ocamlvars.mk
 
 export COQTOP := $(COQ_STDLIB_DIR)
 export COQLIB := $(COQ_STDLIB_DIR)
 export COQBIN := /usr/bin/
 
-PACKAGES := $(shell dh_listpackages)
-
-INSTALL_DIR := $(CURDIR)/debian/tmp/usr/lib/coq/user-contrib/mathcomp
-
-# The following must be kept in sync with d/libssreflect-ocaml*.install.in
-PLUGIN_TARGETS := ssreflect_plugin.cmo
-ifeq ($(OCAML_NATDYNLINK),yes)
-  PLUGIN_TARGETS += ssreflect_plugin.cmxs
-endif
-EXTRA_FILES := ssreflect.cmi ssreflect_plugin.cmi
-
 %:
-	+dh $@ --with ocaml
+	dh $@
 
 .PHONY: override_dh_auto_build
 override_dh_auto_build:
+	$(MAKE) -C mathcomp
 
-# Building is done here because dh_listpackages is useless in the
-# build target. Should be reconsidered when dpkg-buildpackage starts
-# calling build-{arch,indep} targets (see #604397)
 .PHONY: override_dh_auto_install
 override_dh_auto_install:
-ifeq ($(findstring libssreflect-coq,$(PACKAGES)),)
-# Express build: only plugins
-	$(MAKE) -C mathcomp Makefile.coq
-	$(MAKE) -C mathcomp -f Makefile.coq $(PLUGIN_TARGETS)
-	install -d $(INSTALL_DIR)
-	cd mathcomp; \
-		install -m 644 $(PLUGIN_TARGETS) $(EXTRA_FILES) $(INSTALL_DIR)
-else
-# Full build
-	$(MAKE) -C mathcomp
 	$(MAKE) -C mathcomp install DSTROOT=$(CURDIR)/debian/tmp
-	mkdir -p $(CURDIR)/debian/tmp/usr/share/doc/libssreflect-coq/html
-	cp -r htmldoc $(CURDIR)/debian/tmp/html
-endif
-
-.PHONY: override_dh_install
-override_dh_install:
-	dh_install --fail-missing
-
-.PHONY: override_dh_auto_clean
-override_dh_auto_clean:
-	dh_auto_clean
-	rm -Rf bin
 
-.PHONY: override_dh_clean
-override_dh_clean:
-	dh_clean
-	rm -Rf html
+.PHONY: override_dh_missing
+override_dh_missing:
+	dh_missing --fail-missing
 
 .PHONY: override_dh_gencontrol
 override_dh_gencontrol:

debian/tests/control

+Tests: loadssreflect
+Depends: @, coq

debian/tests/loadssreflect

+#!/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