some work on ssreflect and discrete

27 files changed, 1580 insertions, 23 deletions

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..4632509
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,9 @@
+*.d
+*.vo
+*.cm*
+*~
+*.glob
+*.aux
+*.a
+*.o
+Make*.coq
diff --git a/etc/AUTHORS b/etc/AUTHORS
new file mode 100644
index 0000000..848f504
--- /dev/null
+++ b/etc/AUTHORS
@@ -0,0 +1,15 @@
+Andrea Asperti      University of Bologna - Microsoft Inria Joint Centre
+Jeremy Avigad       Carnegie Mellon University - Microsoft Inria Joint Centre
+Yves Bertot         Inria Sophia Antipolis - Microsoft Inria Joint Centre
+Cyril Cohen         LIX École Polytechnique - Microsoft Inria Joint Centre  	
+François Garillot   Microsoft Inria Joint Centre
+Georges Gonthier    Microsoft Research Cambridge - Microsoft Inria Joint Centre
+Stéphane Le Roux    Microsoft Inria Joint Centre
+Assia Mahboubi      Inria Saclay - Microsoft Inria Joint Centre
+Sidi Ould Biha      Inria Sophia Antipolis - Microsoft Inria Joint Centre
+Ioana Pasca         Inria Sophia Antipolis - Microsoft Inria Joint Centre
+Laurence Rideau     Inria Sophia Antipolis - Microsoft Inria Joint Centre
+Alexey Solovyev     University of Pittsburgh
+Enrico Tassi        Inria Saclay - Microsoft Inria Joint Centre
+Laurent Théry       Inria Sophia Antipolis - Microsoft Inria Joint Centre
+Russell O'Connor    Mc Master University - Microsoft Inria Joint Centre
diff --git a/etc/CeCILL-B b/etc/CeCILL-B
new file mode 100644
index 0000000..fe29f5c
--- /dev/null
+++ b/etc/CeCILL-B
@@ -0,0 +1,514 @@
+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/etc/INSTALL b/etc/INSTALL
new file mode 100644
index 0000000..c468b6f
--- /dev/null
+++ b/etc/INSTALL
@@ -0,0 +1,50 @@
+INSTALLATION PROCEDURE FOR THE MATHEMATICAL COMPONENTS LIBRARY
+--------------------------------------------------------------
+
+LINUX AND MAC
+=============
+
+0. Install opam.  Instructions at
+
+     http://opam.ocaml.org/doc/Install.html
+
+1. Be sure to have the Coq stable repository added to opam by typing
+
+     opam repo list
+
+   If it is not the case, type
+
+     opam repo add coq-stable https://github.com/coq/repo-stable.git
+
+2. To find all Mathematical Components libraries type
+
+     opam search coq:mathcomp
+
+3. To get more info about a package type (for example)
+
+     opam show coq:mathcomp:discrete
+
+4. To install the ones you need, type (for example)
+
+     opam install coq:mathcomp:discrete
+
+   To take advantage of parallel hardware one can add
+   the flag -j to specify how many concurrent jobs are
+   run, for example type
+
+     opam install -j2 coq:mathcomp:discrete
+
+5. To remove a package, type (for example)
+
+     opam remove coq:mathcomp:discrete
+
+WINDOWS
+=======
+
+0. Install Coq using the official Windows installer from
+
+    ...
+
+1. Download and install the all in one bundle
+
+    ...
diff --git a/etc/NOTICE b/etc/NOTICE
new file mode 100644
index 0000000..a8dd3a6
--- /dev/null
+++ b/etc/NOTICE
@@ -0,0 +1,2 @@
+(* (c) Copyright Microsoft Corporation and Inria.                       *)
+(* You may distribute this file under the terms of the CeCILL-B license *)
diff --git a/etc/README b/etc/README
new file mode 100644
index 0000000..8cbd1b5
--- /dev/null
+++ b/etc/README
@@ -0,0 +1,40 @@
+          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://ssr.msr-inria.inria.fr/
+
+
+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    
diff --git a/etc/artwork/coqdoc.css b/etc/artwork/coqdoc.css
new file mode 100644
index 0000000..49e87ce
--- /dev/null
+++ b/etc/artwork/coqdoc.css
@@ -0,0 +1,236 @@
+ody { padding: 0px 0px;

+       margin: 0px 0px; 

+       background-color: white }

+

+#page { display: block;

+        padding: 0px;

+        margin: 0px;

+        padding-bottom: 10px; }

+

+#header { display: block;

+          position: relative;

+          padding: 0;

+          margin: 0;

+          vertical-align: middle;

+          border-bottom-style: solid;

+          border-width: thin }

+

+#header h1 { padding: 0; 

+             margin: 0;}

+

+

+/* Contents */

+

+#main{ display: block;

+       padding: 10px;

+       font-family: sans-serif;

+       font-size: 100%;

+       line-height: 100% }

+

+#main  h1 { line-height: 95% } /* allow for multi-line headers */

+

+#main  a.idref:visited {color : #416DFF; text-decoration : none; }

+#main  a.idref:link {color : #416DFF; text-decoration : none; }

+#main  a.idref:hover {text-decoration : none; }

+#main  a.idref:active {text-decoration : none; }

+

+#main  a.modref:visited {color : #416DFF; text-decoration : none; }

+#main  a.modref:link {color : #416DFF; text-decoration : none; }

+#main  a.modref:hover {text-decoration : none; }

+#main  a.modref:active {text-decoration : none; }

+

+#main .keyword { color : #cf1d1d }

+#main { color: black }

+

+.section { background-color: rgb(60%,60%,100%);

+           padding-top: 13px; 

+           padding-bottom: 13px; 

+           padding-left: 3px; 

+           margin-top: 5px;

+           margin-bottom: 5px;

+           font-size : 110% }

+

+h2.section { background-color: rgb(80%,80%,100%);

+             padding-left: 3px; 

+             padding-top: 12px; 

+             padding-bottom: 10px; 

+             font-size : 110% }

+

+h3.section { background-color: rgb(90%,90%,100%);

+             padding-left: 3px; 

+             padding-top: 7px; 

+             padding-bottom: 7px; 

+             font-size : 110% }

+

+h4.section { 

+/*

+                   background-color: rgb(80%,80%,80%);

+                   max-width: 20em;

+                   padding-left: 5px; 

+                   padding-top: 5px; 

+                   padding-bottom: 5px; 

+*/

+                   background-color: white;

+                   padding-left: 0px; 

+                   padding-top: 0px; 

+                   padding-bottom: 0px; 

+                   font-size : 100%;

+                   font-style : bold;

+                   text-decoration : underline;

+ }

+

+#main .doc { margin: 0px;

+             font-family: courier;

+             font-size: 100%;

+	     line-height: 125%;

+             max-width:  50em;

+             color: black;

+	     padding: 10px;

+             background-color: #90bdff;

+             border-style: plain;

+	     white-space: pre;

+     }

+

+.inlinecode { 

+    display: inline;

+/*    font-size: 125%; */

+    color: #666666;

+    font-family: monospace } 

+

+.doc .inlinecode { 

+    display: inline;

+    font-size: 120%; 

+    color: rgb(30%,30%,70%);

+    font-family: monospace } 

+

+.doc .inlinecode .id {

+    color: rgb(30%,30%,70%);

+}

+

+.doc .code { 

+    display: inline;

+    font-size: 120%; 

+    color: rgb(30%,30%,70%); 

+    font-family: monospace } 

+

+.comment { 

+    display: inline;

+    font-family: monospace;

+    color: #cf1d1d

+} 

+

+.code { 

+    display: block;

+/*  padding-left: 15px; */

+    font-size: 110%; 

+    font-family: monospace;

+ } 

+

+/* Pied de page */

+

+#footer { font-size: 65%;

+          font-family: sans-serif; }

+

+.id { display: inline; }

+

+.id[type="constructor"] { 

+    color: rgb(60%,0%,0%);

+}

+

+.id[type="var"] { 

+    color: rgb(40%,0%,40%);

+}

+

+.id[type="variable"] { 

+    color: rgb(40%,0%,40%);

+}

+

+.id[type="definition"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="abbreviation"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="lemma"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="instance"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="projection"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="method"] { 

+    color: rgb(0%,40%,0%);

+}

+

+.id[type="inductive"] { 

+    color: rgb(0%,0%,80%);

+}

+

+.id[type="record"] { 

+    color: rgb(0%,0%,80%);

+}

+

+.id[type="class"] { 

+    color: rgb(0%,0%,80%);

+}

+

+.id[type="keyword"] { 

+ color : #cf1d1d;

+/*     color: black; */

+}

+

+.inlinecode .id {

+    color: rgb(0%,0%,0%);

+}

+

+

+/* TOC */

+

+#toc h2 {

+    padding: 10px;

+    background-color: rgb(60%,60%,100%);

+}

+

+#toc li {

+    padding-bottom: 8px;

+}

+

+/* Index */

+

+#index {

+    margin: 0;

+    padding: 0;

+    width: 100%;

+}

+

+#index #frontispiece {

+    margin: 1em auto;

+    padding: 1em;

+    width: 60%;

+}

+

+.booktitle { font-size : 140%  }

+.authors { font-size : 90%;

+	         line-height: 115%;  }

+.moreauthors { font-size : 60%  }

+

+#index #entrance {

+    text-align: center;

+}

+

+#index #entrance .spacer {

+    margin: 0 30px 0 30px;

+}

+

+#index #footer {

+    position: absolute;

+    bottom: 0;

+    text-align: bottom;

+}


diff --git a/etc/artwork/jc.png b/etc/artwork/jc.png
new file mode 100644
index 0000000..cf90652
--- /dev/null
+++ b/etc/artwork/jc.png
diff --git a/etc/utils/builddoc_lib.sh b/etc/utils/builddoc_lib.sh
new file mode 100644
index 0000000..89d1911
--- /dev/null
+++ b/etc/utils/builddoc_lib.sh
@@ -0,0 +1,146 @@
+
+mangle_sources() {
+# pre processing, mainly comments
+for f in $@; do 
+
+
+sed -r -e '
+        # We remove comments inside proofs 
+       /^Proof.$/,/^Qed./s/\(\*[^*](([^(]|\([^*]){1,}?[^^])\*+\)//g;
+        ' $f |
+
+sed -r -e '
+        # read the whole file into the pattern space
+        # :a is the label, N glues the current line; b branches
+        # to a if not EOF
+        :a; N; $!ba;                                                                                                         
+        # remove all starred lines
+        s/\(\*{5,}?\)//g;
+    
+        # remove *)\n(*
+        s/\*+\)\n\(\*+/\n/g;
+        
+        # double star not too short comments, that are left
+        # as singly starred comments, like (*a.3*)
+        s/\n\(\*+(([^(]|\([^*]){5,}?[^^])\*+\)/\n(**\ \1\ **)/g;
+
+        # restore hide
+        s/\(\*+[ ]*begin hide[ ]*\*+\)/\(\* begin hide \*\)/g;
+        s/\(\*+[ ]*end hide[ ]*\*+\)/\(\* end hide \*\)/g;
+	' |
+
+sed -r -e '
+	# since ranges apply to lines only we create lines
+	s/\(\*\*/\n(**\n/g;
+	s/\*\*\)/\n**)\n/g;
+	' |
+
+sed -r -e '
+	# quote sharp, percent and dollar on comment blocks
+	# hiding underscore
+	/\(\*\*/,/\*\*\)/s/#/##/g;
+	/\(\*\*/,/\*\*\)/s/%/%%/g;
+	/\(\*\*/,/\*\*\)/s/\$/$$/g;
+	/\(\*\*/,/\*\*\)/s/\[/#[#/g;
+	/\(\*\*/,/\*\*\)/s/]/#]#/g;
+	/\(\*\*/,/\*\*\)/s/\_/#\_#/g;
+
+	# the lexer glues sharp with other symbols
+	/\(\*\*/,/\*\*\)/s/([^A-Za-z0-9 ])#\[#/\1 #[#/g;
+	/\(\*\*/,/\*\*\)/s/([^A-Za-z0-9 ])#]#/\1 #]#/g;
+	' |
+
+sed -r -e '
+	# we glue comment lines back together
+        :a; N; $!ba; 
+	s/\n\(\*\*\n/(**/g;
+	s/\n\*\*\)\n/**)/g;
+	' > $f.tmp
+	mv $f.tmp $f
+done
+}
+
+build_doc() {
+rm -rf html
+mkdir html
+coqdoc -t "$TITLE" -g --utf8 $COQDOCOPTS \
+        --parse-comments \
+	--multi-index $@ -d html
+
+# graph
+coqdep -noglob $COQOPTS $@ > depend
+sed -i -e 's/ [^ ]*\.cmxs//g' -e 's/ [^ ]*\.cm.//g' depend
+ocamlc -o $MAKEDOT/makedot -pp camlp5o $MAKEDOT/dependtodot.ml
+$MAKEDOT/makedot depend
+mv *.dot theories.dot || true
+$MANGLEDOT theories.dot
+dot -Tpng -o html/depend.png -Tcmapx -o html/depend.map theories.dot
+dot -Tsvg -o html/depend.svg theories.dot
+
+# post processing
+for f in html/*.html; do sed -r -i -e '
+	# read the whole file into the pattern space
+	# :a is the label, N glues the current line; b branches
+	# to a if not EOF
+	:a; N; $!ba;
+
+        #Add the favicon
+        s/^<\/head>/<link rel="icon" type="image\/png" href="favicon.png" \/>\n<\/head>/mg;
+
+	# add the Joint Center logo
+	s/<h1([^>]*?)>/<h1\1><img src="jc.png" alt="(Joint Center)"\/>/g;
+
+	# extra blank line
+    	s/<div\ class="doc">\n/<div class="doc">/g;
+
+	# weird underscore
+    	s/ /_/g;
+ 
+        # putting back underscore
+	s/#\_#/\_/g;
+
+
+	# abundance of <br/>
+    	s/\n<br\/> <br\/>//g;
+	' $f
+done
+
+mv html/index.html html/index_lib.html
+cat >html/index.html <<EOT
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
+"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
+<link href="coqdoc.css" rel="stylesheet" type="text/css"/>
+<link rel="icon" type="image/png" href="favicon.png" />
+<title>$TITLE</title>
+</head>
+
+<body>
+
+<div id="page">
+
+<div id="header">
+</div>
+
+<div id="main">
+
+<h1><img src="jc.png" alt="(Joint Center)"/>
+$TITLE Documentation</h1>
+<hr/>
+<img class="graph" src="depend.png" usemap="#theories" />
+EOT
+cat html/depend.map >> html/index.html
+cat >>html/index.html <<EOT
+<hr/>
+<center><a href="index_lib.html">
+Library index
+</a></center>
+</div>
+</div>
+</body>
+</html>
+EOT
+
+}
diff --git a/etc/utils/dependtodot.ml b/etc/utils/dependtodot.ml
new file mode 100644
index 0000000..1ea350f
--- /dev/null
+++ b/etc/utils/dependtodot.ml
@@ -0,0 +1,343 @@
+(* Loic Pottier, projet CROAP, INRIA Sophia Antipolis, April 1998. *)
+(* Laurent Théry , INRIA Sophia Antipolis, April 2007 *)
+
+(* Convert a dependencies file, in makefile form, into a graph in a file readable by dot.
+
+The function dependtodot takes as input the dependencies file, and create a file with the same name suffixed by ".dot", readable by  dot.
+
+*)
+
+let nodecol="#dbc3b6";; (* #add8ff *)
+let edgecol="#676767";; (* #ff0000 *)
+
+(* parameters to draw edges and nodes *)
+let vnode x = 
+    "l(\"" ^ x 
+    ^ "\",n(\"\",[a(\"COLOR\",\""^ nodecol ^"\"),a(\"OBJECT\",\"" ^ x ^ "\")],"
+;;
+
+let wstring x = "\""^x^"\""
+;;
+
+let vnoder x = "r(\"" ^ x ^ "\")"
+;;
+
+let vedge = 
+  "e(\"\",[a(\"_DIR\",\"inverse\"),a(\"EDGEPATTERN\",\"solid\"),a(\"EDGECOLOR\",\"" ^ edgecol ^ "\")],"
+;;
+    
+let listdv l = match l with
+    [] -> "[]"
+   |x::l -> let rec listdvr l = match l with
+                                [] -> ""
+                               |y::l -> "," ^ y ^ (listdvr l)
+            in "[" ^ x ^ (listdvr l) ^ "]"
+;;
+
+let rec visit ht hte x s =
+          Hashtbl.add ht x x;
+          try let le=Hashtbl.find hte x in
+              let rec visit_edge ls le =
+                 match le with
+                   [] -> ls
+                  |b::l -> 
+                     try let _ =Hashtbl.find ht b in
+                           (visit_edge (ls@[vedge ^ (vnoder b) ^ ")"]) l)
+                     with Not_found ->
+                       (visit_edge (ls@[vedge ^ (visit ht hte b s) ^ ")"]) l)
+              in s ^ (vnode x) ^ (listdv (visit_edge [] le)) ^ "))"
+          with Not_found -> s ^ (vnode x) ^ "[]))"
+;;
+
+(* cloture transitive *)
+
+let rec merge_list a b = match a with
+    [] -> b
+   |x::a -> if (List.mem x b) 
+            then (merge_list a b)
+            else x::(merge_list a b)
+;;
+
+let ht_graph g =
+  let ht =Hashtbl.create 50 in
+  let rec fill g = match g with
+        [] -> ()
+       |(a,lb)::g -> Hashtbl.add ht a lb; fill g
+  in fill g;
+  ht
+;;
+
+let trans_clos1 g =
+  let ht =ht_graph g in
+  List.map (fun (a,lb) -> 
+     (a,(let l = ref lb in
+         let rec addlb lb = match lb with
+           [] -> ()
+          |b::lb -> (try l:=(merge_list (Hashtbl.find ht b) !l)
+                     with Not_found -> ()); addlb lb
+         in addlb lb;
+         !l))) g
+;;
+
+let rec transitive_closure g =
+  let g1=trans_clos1 g in
+  if g1=g then g else (transitive_closure g1)
+;;
+
+(*
+let g=["A",["B"];
+       "B",["C"];
+       "C",["D"];
+       "D",["E"];
+       "E",["A"]];;
+transitive_closure g;;
+*)
+
+(* enlever les arcs de transitivite *)
+
+let remove_trans g =
+  let ht = ht_graph (transitive_closure g) in
+  List.map (fun (a,lb) ->
+   (a,(let l=ref [] in
+       (let rec sel l2 = match l2 with
+          [] -> ()
+         |b::l2 -> (let r=ref false in
+                    (let rec testlb l3 = match l3 with
+                         [] -> ()
+                        |c::l3 -> if (not (b=a)) &&(not(b=c)) && (not (a=c)) &&
+                                     (try (List.mem b (Hashtbl.find ht c))
+                                      with Not_found -> false)
+                                  then r:=true
+                                  else ();
+                                  testlb l3
+                    in testlb lb);
+                    if (!r=false)
+                    then l:=b::!l
+                    else ());
+                    sel l2
+        in sel lb);
+        !l))) g
+;;
+         
+(*
+let g1=["Le", ["C";"Lt";"B"; "Plus"];
+  "Lt", ["A";"Plus"]];;
+
+let g=["A",["B";"C";"D";"E"];
+       "B",["C"];
+       "C",["D"];
+       "D",["E"]];;
+remove_trans g;;
+
+*)         
+let dot g name file=
+   let chan_out = open_out  (file^".dot") in
+   output_string chan_out "digraph ";
+   output_string chan_out name;
+   output_string chan_out " {\n";
+   output_string chan_out "  bgcolor=transparent;\n";
+   output_string chan_out "  splines=true;\n";	
+   output_string chan_out "  nodesep=1;\n";	
+   output_string chan_out "  node [fontsize=18, shape=rect, color=\"#dbc3b6\", style=filled];\n";
+   List.iter (fun (x,y) -> 
+        output_string chan_out "  ";
+        output_string chan_out (wstring x);
+        output_string chan_out " [URL=\"./";
+        output_string chan_out x;
+        output_string chan_out ".html\"]\n";
+     List.iter (fun y ->
+                     output_string chan_out "  ";
+                     output_string chan_out (wstring x);
+                     output_string chan_out " -> ";
+                     output_string chan_out (wstring y);
+                     output_string chan_out ";\n") y) g;
+   flush chan_out;
+   output_string chan_out "}";
+   close_out  chan_out
+;;
+
+(*
+example: a complete 5-graph,
+
+let g=["A",["B";"C";"D";"E"];
+       "B",["A";"C";"D";"E"];
+       "C",["A";"B";"D";"E"];
+       "D",["A";"B";"C";"E"];
+       "E",["A";"B";"C";"D"]];;
+
+daVinci g "g2";;
+
+the file is then g2.daVinci
+
+*)
+(***********************************************************************)
+open Genlex;;
+
+(* change OP april 28 *)
+(* 
+this parsing produce a pair where the first member is a paire (file,Directory) 
+and the second is a list of pairs (file,Directory).
+from this we can compute the files graph dependency and also the directory graph dependency
+*)
+
+let lexer = make_lexer [":";".";"/";"-"];; 
+
+let rec parse_dep = parser
+    [< a=parse_name; 'Kwd ".";'Ident b; _=parse_until_colon;
+      _=parse_name ;'Kwd "."; 'Ident d;n=parse_rem  >] -> (a,n)
+and parse_rem = parser
+    [< a=parse_name;'Kwd ".";'Ident b;n=parse_rem >] -> a::n
+    | [<>]->[]
+and parse_until_colon = parser
+     [< 'Kwd ":" >] -> ()
+   | [< 'Kwd _; _=parse_until_colon >] -> ()
+   | [< 'Int _; _=parse_until_colon >] -> ()
+   | [< 'Ident _; _=parse_until_colon >] -> ()
+
+and parse_name = parser
+   [<'Kwd "/";a=parse_ident; b=parse_name_rem a "" >]-> a::b
+  |[<a=parse_ident; b=parse_name_rem a "" >]-> a::b
+ and parse_name2 k = parser
+   [<d=parse_ident; b=parse_name_rem d k >]-> d::b
+ and parse_name_rem a b= parser
+     [<'Kwd "/";c=parse_name2 a >]-> c
+   | [<>]->[]
+
+and parse_ident = parser
+   [<'Ident a; b=parse_ident_rem a "" >]-> a ^ b
+  |[<'Int a; b=parse_ident_rem (string_of_int a) "" >]-> (string_of_int a) ^ b
+ and parse_ident2 k = parser
+   [<'Ident d; b=parse_ident_rem d k >]-> d ^ b
+  |[<'Int d; b=parse_ident_rem (string_of_int d) k >]-> (string_of_int d) ^ b
+ and parse_ident_rem a b= parser
+     [<'Kwd "-";c=parse_ident2 a >]-> "-" ^ c
+   | [<>]-> ""
+;;
+
+(*
+parse_name(lexer(Stream.of_string "u/sanglier/0/croap/pottier/Coq/Dist/contrib/Rocq/ALGEBRA/CATEGORY_THEORY/NT/YONEDA_LEMMA/NatFun.vo: "));;
+parse_ident(lexer(Stream.of_string "ARITH-OMEGA-ggg-2.vo:"));; PROBLEME
+*)
+
+(* reads the depend file *)
+let read_depend file=
+  let st =open_in file in
+  let lr =ref [] in
+  let rec other() =
+       (try 
+         let d=parse_dep(lexer(Stream.of_string (input_line st))) in
+         lr:=d::(!lr);
+         other()
+        with _ ->[]) 
+   in (let _ = other() in ());
+   !lr;;
+
+(* graph of a directory (given by a path) *)
+let rec is_prefix p q = match p with
+   [] -> true
+  |a::p -> match q with [] -> false
+                       |b::q -> if a=b then (is_prefix p q) else false
+;;
+  
+let rec after_prefix p q = match p with
+   [] ->(match q with
+            [] -> "unknown"
+           |a::_ -> a)
+  |a::p -> match q with [] -> "unknown"
+                       |b::q -> (after_prefix p q)
+;;
+
+let rec proj_graph p g =  match g with
+  [] -> []
+ |(q,l)::g -> if (is_prefix p q) 
+           then let rec proj_edges l = match l with
+                     [] -> []
+		    |r::l -> if (is_prefix p r)
+		             then (after_prefix p r)::(proj_edges l)
+                             else (proj_edges l)
+                in ((after_prefix p q),(proj_edges l))
+                   ::(proj_graph p g)
+           else (proj_graph p g)
+
+;;
+
+let rec start_path p = match p with
+   [] ->[]
+  |a::p -> match p with
+              [] ->[]
+             |b::q -> a::(start_path p)
+;;
+
+  
+(* the list of all the paths and subpaths in g *)
+let all_path g =
+   let ht =Hashtbl.create 50 in
+   let add_path p = Hashtbl.remove ht p;Hashtbl.add ht p true in
+   let rec add_subpath p = match p with
+          [] ->()
+         |_ -> add_path p; add_subpath (start_path p) in      
+   let rec all_path g = match g with
+      [] -> ()
+     |(q,l)::g -> add_subpath (start_path q);
+                  let rec all_pathl l = match l with
+                       [] -> ()
+                      |a::l -> add_subpath (start_path a);
+                               all_pathl l
+                  in all_pathl l;
+                  all_path g
+   in all_path g;
+   let lp=ref [] in
+     Hashtbl.iter (fun x y -> lp:=x::!lp) ht;
+     !lp
+;;
+                     
+    
+(*
+let g=read_depend "depend";;
+proj_graph ["theories"] g;;
+*)
+
+let rec endpath p =  match p with
+   [] ->""
+  |a::p -> match p with
+                [] ->a
+               |_ -> endpath p
+;;
+
+let rec fpath p =  match p with
+   [] ->""
+  |a::p -> a ^ "/" ^ (fpath p)
+;;
+
+let rec spath p = match p with
+   [] -> ""
+  |a::p -> match p with
+                [] ->a
+               |b::q -> a ^ "/" ^ (spath p)
+;;
+
+(* creates graphs for all paths *)
+
+
+let dependtodot file=
+  let g =(read_depend file) in
+  let lp1 = all_path g in
+  let lp = (if lp1=[] then [[]] else lp1) in
+  let rec ddv lp = match lp with
+     [] -> ()
+    |p::lp -> let name =  (let f = (endpath p) in
+                           if f="" then file else f) in
+              let filep = (let f = (spath p) in
+                           if f="" then file else f) in
+              dot (remove_trans (proj_graph p g)) 
+                    name filep;
+              ddv lp
+  in ddv lp
+  
+;;
+let _ = 
+  if (Array.length Sys.argv) == 2 then
+    dependtodot Sys.argv.(1)
+  else print_string "makedot depend";
+       print_newline()
+
diff --git a/etc/win-installer.nsi b/etc/win-installer.nsi
new file mode 100755
index 0000000..8562acc
--- /dev/null
+++ b/etc/win-installer.nsi
@@ -0,0 +1,115 @@
+SetCompressor lzma
+
+; The VERSION should be passed as an argument at compile time using :
+;      nsis -DVERSION=1.5 win-installer.nsi
+
+!define MY_PRODUCT "Coq" ;Define your own software name here
+!define SRC ".\"
+!define SRC_SSR "C:\Coq\lib\user-contrib\Ssreflect\"
+!define SRC_MC "C:\Coq\lib\user-contrib\MathComp\"
+!define OUTFILE "ssr-mathcomp-installer-${VERSION}.exe"
+
+!include "MUI2.nsh"
+
+;--------------------------------
+;Configuration
+
+  Name "Ssreflect and the Mathematical Components library"
+
+  ;General
+  OutFile "${OUTFILE}"
+
+  ;Folder selection page
+  InstallDir "C:\Coq"
+  
+  ;Remember install folder
+  InstallDirRegKey HKCU "Software\Coq" ""
+
+;--------------------------------
+;Modern UI Configuration
+
+  !insertmacro MUI_PAGE_WELCOME
+  !insertmacro MUI_PAGE_LICENSE "${SRC}\CeCILL-B"
+  !insertmacro MUI_PAGE_COMPONENTS
+  !define MUI_DIRECTORYPAGE_TEXT_TOP "Select where Coq is installed."
+  !insertmacro MUI_PAGE_DIRECTORY
+  !insertmacro MUI_PAGE_INSTFILES
+  !insertmacro MUI_PAGE_FINISH
+  
+  !insertmacro MUI_UNPAGE_WELCOME
+  !insertmacro MUI_UNPAGE_CONFIRM
+  !insertmacro MUI_UNPAGE_INSTFILES
+  !insertmacro MUI_UNPAGE_FINISH  
+
+;--------------------------------
+;Languages
+ 
+  !insertmacro MUI_LANGUAGE "English"
+  
+;--------------------------------
+;Language Strings
+
+  ;Description
+  LangString DESC_1 ${LANG_ENGLISH} "This package contains the Ssreflect proof language."
+  LangString DESC_2 ${LANG_ENGLISH} "This package contains the Mathematical Components lirbary."
+
+;--------------------------------
+;Installer Sections
+
+
+Section "Ssreflect" Sec1
+
+  SetOutPath "$INSTDIR\lib\user-contrib\Ssreflect\"
+
+  File /r ${SRC_SSR}\*.vo
+  File /r ${SRC_SSR}\*.v
+  File /r ${SRC_SSR}\*.glob
+  File /r ${SRC_SSR}\*.cmx
+  File /r ${SRC_SSR}\*.cmxs
+  File /r ${SRC_SSR}\*.cmi
+
+  CreateDirectory "$SMPROGRAMS\Coq"
+
+  WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/ssreflect-${VERSION}/"
+
+  WriteINIStr "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url" "InternetShortcut" "URL" "http://hal.inria.fr/inria-00258384/en"
+        
+  SetOutPath "$INSTDIR"
+  writeUninstaller "Uninstall Ssreflect and MathComp.exe"
+
+SectionEnd
+
+Section "MathComp" Sec2
+
+  SetOutPath "$INSTDIR\lib\user-contrib\MathComp\"
+
+  File /r ${SRC_MC}\*.vo
+  File /r ${SRC_MC}\*.v
+  File /r ${SRC_MC}\*.glob
+  File /r ${SRC_MC}\*.cmx
+  File /r ${SRC_MC}\*.cmxs
+  File /r ${SRC_MC}\*.cmi
+
+  CreateDirectory "$SMPROGRAMS\Coq"
+
+  WriteINIStr "$SMPROGRAMS\Coq\The Mathematical Components Library.url" "InternetShortcut" "URL" "http://ssr.msr-inria.inria.fr/doc/mathcomp-${VERSION}/"
+
+SectionEnd
+
+!insertmacro MUI_FUNCTION_DESCRIPTION_BEGIN
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec1} $(DESC_1)
+  !insertmacro MUI_DESCRIPTION_TEXT ${Sec2} $(DESC_2)
+!insertmacro MUI_FUNCTION_DESCRIPTION_END
+ 
+Section "Uninstall"
+
+  RMDir /r "$INSTDIR\lib\user-contrib\MathComp\"
+  RMDir /r "$INSTDIR\lib\user-contrib\Ssreflect\"
+
+  Delete "$SMPROGRAMS\Coq\The Mathematical Components Library.url"
+  Delete "$SMPROGRAMS\Coq\The Ssreflect Library.url"
+  Delete "$SMPROGRAMS\Coq\The Ssreflect User Manaul.url"
+
+  Delete "$INSTDIR\Uninstall Ssreflect and MathComp.exe"
+  
+SectionEnd
diff --git a/mathcomp/discrete/AUTHORS b/mathcomp/discrete/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/discrete/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/discrete/CeCILL-B b/mathcomp/discrete/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/discrete/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/discrete/INSTALL b/mathcomp/discrete/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/discrete/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/discrete/Make b/mathcomp/discrete/Make
new file mode 100644
index 0000000..bfbbfe2
--- /dev/null
+++ b/mathcomp/discrete/Make
@@ -0,0 +1,15 @@
+all.v
+bigop.v
+binomial.v
+choice.v
+div.v
+finfun.v
+fingraph.v
+finset.v
+fintype.v
+generic_quotient.v
+path.v
+prime.v
+tuple.v
+
+-R . mathcomp.discrete
diff --git a/mathcomp/discrete/Makefile b/mathcomp/discrete/Makefile
new file mode 100644
index 0000000..d693257
--- /dev/null
+++ b/mathcomp/discrete/Makefile
@@ -0,0 +1,23 @@
+H=@
+
+ifeq "$(COQBIN)" ""
+COQBIN=$(dir $(shell which coqtop))/
+endif
+
+
+OLD_MAKEFLAGS:=$(MAKEFLAGS)
+MAKEFLAGS+=-B
+
+.DEFAULT_GOAL := all
+
+%:
+	$(H)[ -e Makefile.coq ] || $(COQBIN)/coq_makefile -f Make -o Makefile.coq
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq $*
+
+.PHONY: clean
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
+
diff --git a/mathcomp/discrete/README b/mathcomp/discrete/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/discrete/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/discrete/all.v b/mathcomp/discrete/all.v
index d100add..8412bdb 100644
--- a/mathcomp/discrete/all.v
+++ b/mathcomp/discrete/all.v
@@ -1,12 +1,13 @@
-Require Export bigop.
-Require Export binomial.
+Require Export mathcomp.ssreflect.all.
 Require Export choice.
+Require Export path.
 Require Export div.
-Require Export finfun.
+Require Export fintype.
 Require Export fingraph.
+Require Export tuple.
+Require Export finfun.
+Require Export bigop.
+Require Export prime.
 Require Export finset.
-Require Export fintype.
+Require Export binomial.
 Require Export generic_quotient.
-Require Export path.
-Require Export prime.
-Require Export tuple.
diff --git a/mathcomp/discrete/opam b/mathcomp/discrete/opam
new file mode 100644
index 0000000..3646845
--- /dev/null
+++ b/mathcomp/discrete/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:discrete"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/discrete'" ]
+depends: [ "coq:mathcomp:ssreflect" { = "1.5" } ]
diff --git a/mathcomp/ssreflect/AUTHORS b/mathcomp/ssreflect/AUTHORS
new file mode 120000
index 0000000..b55a98d
--- /dev/null
+++ b/mathcomp/ssreflect/AUTHORS
@@ -0,0 +1 @@
+../../etc/AUTHORS
\ No newline at end of file
diff --git a/mathcomp/ssreflect/CeCILL-B b/mathcomp/ssreflect/CeCILL-B
new file mode 120000
index 0000000..83e22fd
--- /dev/null
+++ b/mathcomp/ssreflect/CeCILL-B
@@ -0,0 +1 @@
+../../etc/CeCILL-B
\ No newline at end of file
diff --git a/mathcomp/ssreflect/INSTALL b/mathcomp/ssreflect/INSTALL
new file mode 120000
index 0000000..6aa7ec5
--- /dev/null
+++ b/mathcomp/ssreflect/INSTALL
@@ -0,0 +1 @@
+../../etc/INSTALL
\ No newline at end of file
diff --git a/mathcomp/ssreflect/Make b/mathcomp/ssreflect/Make
index 9e7c5db..6c76897 100644
--- a/mathcomp/ssreflect/Make
+++ b/mathcomp/ssreflect/Make
@@ -6,3 +6,11 @@ ssreflect.v
 ssrfun.v
 ssrmatching.v
 ssrnat.v
+
+ssreflect.mllib
+ssrmatching.mli
+ssrmatching.ml4
+ssreflect.ml4
+
+-I .
+-R . mathcomp.ssreflect
diff --git a/mathcomp/ssreflect/Makefile b/mathcomp/ssreflect/Makefile
index 46a2d69..12c71fc 100644
--- a/mathcomp/ssreflect/Makefile
+++ b/mathcomp/ssreflect/Makefile
@@ -1,3 +1,5 @@
+H=@
+
 ifeq "$(COQBIN)" ""
 COQBIN=$(dir $(shell which coqtop))/
 endif
@@ -13,21 +15,28 @@ endif
 OLD_MAKEFLAGS:=$(MAKEFLAGS)
 MAKEFLAGS+=-B
 
+.DEFAULT_GOAL := all
+
 %:
-	@[ -e Makefile.coq ] || $(call coqmakefile)
-	@[ Make -ot Makefile.coq ] || $(call coqmakefile)
-	@MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
-		-f Makefile.coq $*
+	$(H)[ -e Makefile.coq ] || $(call coqmakefile)
+# Override COQLIBS to find the "right" copy .ml files, otherwise
+# coq_makefile uses only the -R in COQLIBS and ignores the -I in
+# OCAMLLIBS to look for .ml files in order to generate .d files
+# via coqdep
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq $* \
+		COQLIBS='-I . -R . mathcomp.ssreflect'
 
 define coqmakefile
 	(echo "Generating Makefile.coq for Coq $(V) with COQBIN=$(COQBIN)";\
-	cp Make Make.coq;\
-	echo -I plugin/$(V)/src >> Make.coq;\
-	echo plugin/$(V)/src/ssreflect.mllib >> Make.coq;\
-	echo plugin/$(V)/src/ssrmatching.mli >> Make.coq;\
-	echo plugin/$(V)/src/ssrmatching.ml4 >> Make.coq;\
-	echo plugin/$(V)/src/ssreflect.ml4 >> Make.coq;\
-	$(COQBIN)/coq_makefile -f Make.coq -o Makefile.coq)
+	ln -sf plugin/$(V)/ssreflect.mllib .;\
+	ln -sf plugin/$(V)/ssrmatching.mli .;\
+	ln -sf plugin/$(V)/ssrmatching.ml4 .;\
+	ln -sf plugin/$(V)/ssreflect.ml4 .;\
+	$(COQBIN)/coq_makefile -f Make -o Makefile.coq)
 endef
 
-
+clean:
+	$(H)MAKEFLAGS=$(OLD_MAKEFLAGS) $(MAKE) --no-print-directory \
+		-f Makefile.coq clean
+	$(H)rm -f Makefile.coq
diff --git a/mathcomp/ssreflect/README b/mathcomp/ssreflect/README
new file mode 120000
index 0000000..e4e30e8
--- /dev/null
+++ b/mathcomp/ssreflect/README
@@ -0,0 +1 @@
+../../etc/README
\ No newline at end of file
diff --git a/mathcomp/ssreflect/all.v b/mathcomp/ssreflect/all.v
index c441810..ce3e470 100644
--- a/mathcomp/ssreflect/all.v
+++ b/mathcomp/ssreflect/all.v
@@ -1,7 +1,6 @@
-Require Export eqtype.
-Require Export seq.
-Require Export ssrbool.
 Require Export ssreflect.
+Require Export ssrbool.
 Require Export ssrfun.
-Require Export ssrmatching.
+Require Export eqtype.
 Require Export ssrnat.
+Require Export seq.
diff --git a/mathcomp/ssreflect/opam b/mathcomp/ssreflect/opam
new file mode 100644
index 0000000..bef7ebd
--- /dev/null
+++ b/mathcomp/ssreflect/opam
@@ -0,0 +1,12 @@
+opam-version: "1.2"
+name: "coq:mathcomp:ssreflect"
+version: "1.5"
+maintainer: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+authors: "Ssreflect <ssreflect@msr-inria.inria.fr>"
+homepage: "http://ssr.msr-inria.inria.fr/"
+bug-reports: "ssreflect@msr-inria.inria.fr"
+license: "CeCILL-B"
+build: [ make "-j" "%{jobs}%" ] 
+install: [ make "install" ]
+remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/mathcomp/ssreflect'" ]
+depends: [ "coq" { ( >= "8.4pl4" & < "8.5" ) | ( = "8.5beta1" ) } ]