diff options
| author | Cyril Cohen | 2019-07-02 22:29:07 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2019-09-05 13:59:04 +0200 |
| commit | dd82aaeae7e9478efc178ce8430986649555b032 (patch) | |
| tree | 0deaa7cf99f7417d1623d69cc32b931fffd20e06 /docs/index.html | |
| parent | ba669012734dc17a1050b49121009d083f346303 (diff) | |
Redirects to math-comp.github.io
Merge only after solving issue https://github.com/math-comp/math-comp/issues/361
Diffstat (limited to 'docs/index.html')
| -rw-r--r-- | docs/index.html | 106 |
1 files changed, 1 insertions, 105 deletions
diff --git a/docs/index.html b/docs/index.html index 2ee5b07..cb1939b 100644 --- a/docs/index.html +++ b/docs/index.html @@ -1,106 +1,2 @@ <!doctype html> -<html> - <head> - <meta charset="utf-8"> - <meta http-equiv="X-UA-Compatible" content="chrome=1"> - <title>Mathematical Components</title> - - <link rel="stylesheet" href="stylesheets/styles.css"> - <link rel="stylesheet" href="stylesheets/github-light.css"> - <meta name="viewport" content="width=device-width"> - <!--[if lt IE 9]> - <script src="//html5shiv.googlecode.com/svn/trunk/html5.js"></script> - <![endif]--> - </head> - <body> - <div class="wrapper"> - <header> - <h1>Mathematical Components</h1> - <p> Libraries of formalized mathematics</p> - - <p class="view"><a href="https://github.com/math-comp/math-comp">View the Project on GitHub <small>math-comp/math-comp</small></a></p> - - - <!-- <ul> --> - <!-- <li><a href="https://github.com/math-comp/math-comp/zipball/master">Download <strong>ZIP File</strong></a></li> --> - <!-- <li><a href="https://github.com/math-comp/math-comp/tarball/master">Download <strong>TAR Ball</strong></a></li> --> - <!-- <li><a href="https://github.com/math-comp/math-comp">View On <strong>GitHub</strong></a></li> --> - <!-- </ul> --> - </header> - - <section> - <h3> -<a id="about" class="anchor" href="#about" aria-hidden="true"><span class="octicon octicon-link"></span></a>About</h3> - -<p> The Mathematical Components library for - <a href="http://coq.inria.fr">Coq</a> has its origins in -the formal proof of the Four Colour Theorem. Since then it has grown -to cover many areas of mathematics and has been used for -large scale projects like the formal proof of the Odd Order Theorem. -</p><p> -The library is written using the Ssreflect proof language that is an integral -part of the distribution. -</p> - -<h3> -<a id="releases" class="anchor" href="#releases" aria-hidden="true"><span class="octicon octicon-link"></span></a>Getting the library</h3> - -<p> The current stable release of the -Mathematical Components library can be -<a href="https://github.com/math-comp/math-comp/releases">downloaded from github</a>. -<br/> -Older versions of the library are available -in the <a href="http://ssr.msr-inria.inria.fr/FTP/">historic archive</a>. -</p> - -<h3> -<a id="documentation" class="anchor" href="#documentation" aria-hidden="true"><span class="octicon octicon-link"></span></a>Documentation</h3> - -<p> -Each source files features a documentation header which -describes the concepts and notations introduced in that file. -The <a href="htmldoc/index.html">coqdoc presentation</a> of the source files can be browsed online. -</p> -<p> -The <a href="htmldoc/libgraph.html">library graph</a> can be browsed interactively. -</p> -<p> -The Ssreflect language comes with a dedicated -<a href="http://hal.inria.fr/inria-00258384/en">reference manual</a>. -</p> -<p>We also wrote a <a href="https://math-comp.github.io/mcb/">book</a> introducing the techniques for writing -algorithms and proofs and describing the design ideas of the library. -</p> -<h3> -<a id="contact" class="anchor" href="#contact" aria-hidden="true"><span class="octicon octicon-link"></span></a>Contact</h3> - -<p> -Interested? -<a href="mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect">Subscribe to the ssreflect mailing list</a> -and let us know what you are using our libraries for, ask questions, etc. -You can also browse the <a href="https://sympa.inria.fr/sympa/arc/ssreflect">archives of the list</a> or consult the -<a href="https://sympa.inria.fr/sympa/info/ssreflect">general information page</a>. -</p> -<h3> -<a id="authors-and-contributors" class="anchor" href="#authors-and-contributors" aria-hidden="true"><span class="octicon octicon-link"></span></a>Authors and Contributors</h3> - -<p> The Mathematical Components library and the Ssreflect proof language -are developed by the -<a href="http://www.msr-inria.fr/projects/mathematical-components-2/">Mathematical Components team</a>, at the -<a href="http://www.msr-inria.fr/">Inria -- Microsoft Research Joint Centre</a>. -</p> - <p style="text-align:center;"> - <a href="http://www.msr-inria.fr/"><img src="./logo-MS-Research-Inria-Joint-Centre.png" alt="Microsoft Research - Inria Joint Centre" style="width:50%;margin-left:auto;margin-right:auto;"/></a> - </p> - - </section> - - <footer> - <p><small>Theme by <a href="https://github.com/orderedlist">orderedlist</a></small></p> - </footer> - - </div> - <script src="javascripts/scale.fix.js"></script> - - </body> -</html> +<html><head><meta http-equiv="refresh" content="0; url=http://math-comp.github.io/" /></head></html> |