diff --git a/news/coq-8-12-2-is-out b/news/coq-8-12-2-is-out index 68974131b8..c811f62d47 100644 --- a/news/coq-8-12-2-is-out +++ b/news/coq-8-12-2-is-out @@ -10,7 +10,7 @@ href="https://github.com/coq/coq/releases/tag/V8.12.2">release of Coq

This release fixes two impacting 8.12 regressions (in notations and the implicit argument inference of the exists tactic). See the changelog +href="https://coq.github.io/doc/V8.12.2/refman/changes.html#changes-in-8-12-2">changelog for details.

\ No newline at end of file diff --git a/news/coq-83-beta-version b/news/coq-83-beta-version index da94425a4d..6db20eb741 100644 --- a/news/coq-83-beta-version +++ b/news/coq-83-beta-version @@ -3,7 +3,7 @@ <#def AUTHOR>coq-www <#def DATE>16 Feb 2010 17:44 GMT <#def DESCR> -

The Coq developpers are pleased to announce the release of the beta version of Coq 8.3. This release intends to give the curious and impatient users of Coq a flavour of what Coq 8.3 will be. To see what is new in this version of Coq, please refer to the CHANGES file.

+

The Coq developpers are pleased to announce the release of the beta version of Coq 8.3. This release intends to give the curious and impatient users of Coq a flavour of what Coq 8.3 will be. To see what is new in this version of Coq, please refer to the CHANGES file.

Please be aware that this release should be considered as unstable, and should not be used as a production environment.

-

Now that you have been warned, you can download the source files.

+

Now that you have been warned, you can download the source files.

diff --git a/news/coq-83-is-out b/news/coq-83-is-out index dfae58d090..b186d9cb9d 100644 --- a/news/coq-83-is-out +++ b/news/coq-83-is-out @@ -15,8 +15,8 @@
  • interactive proofs in module types,
  • a beautifying coqc option for pretty-printing files
    • -

    See the file CHANGES for a full log of changes.

    -

    Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting adequate options. See COMPATIBILITY for details and migration recommendations.

    +

    See the file CHANGES for a full log of changes.

    +

    Even if we try to preserve compatibility as much as possible with Coq 8.2, we had to arbitrate for a break of behavior in some situations. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting adequate options. See COMPATIBILITY for details and migration recommendations.

    In addition to the "ssreflect" plugin, extension packages we are aware about include the following (but probably there are more):

    More information about the changes from 8.4 to 8.5 can be found in the -CHANGES file. Feedback and +CHANGES file. Feedback and bug reports are extremely welcome. Enjoy! diff --git a/news/coq-85beta1-is-out b/news/coq-85beta1-is-out index baf8ac3348..5084704c2d 100644 --- a/news/coq-85beta1-is-out +++ b/news/coq-85beta1-is-out @@ -22,6 +22,6 @@ testing. The 8.5 version brings several major features to Coq: More information about the changes from 8.4 to 8.5 can be found in -the CHANGES file. Feedback and +the CHANGES file. Feedback and bug reports are extremely welcome. Enjoy! diff --git a/news/coq-85beta2-is-out b/news/coq-85beta2-is-out index 35fc9b8370..29c79344b5 100644 --- a/news/coq-85beta2-is-out +++ b/news/coq-85beta2-is-out @@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq: More information about the changes from 8.4 to 8.5 and since the first beta release can be found in the CHANGES file. Feedback and CHANGES file. Feedback and bug reports are extremely welcome. Enjoy! diff --git a/news/coq-85beta3-is-out b/news/coq-85beta3-is-out index 4d37e3e2a8..e1f29faed8 100644 --- a/news/coq-85beta3-is-out +++ b/news/coq-85beta3-is-out @@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq: More information about the changes from 8.4 to 8.5 and since the first two beta releases can be found in the CHANGES file. Feedback and CHANGES file. Feedback and bug reports are extremely welcome. Enjoy! diff --git a/news/coq-85pl1-is-out b/news/coq-85pl1-is-out index 4f6cf60c25..4a628013fb 100644 --- a/news/coq-85pl1-is-out +++ b/news/coq-85pl1-is-out @@ -6,6 +6,6 @@ Version 8.5pl1 of Coq is available. It fixes several bugs of version 8.5, including one critical bug. It also brings various performance improvements. More information can be found in the CHANGES file. Feedback and CHANGES file. Feedback and bug reports are extremely welcome. diff --git a/news/coq-85pl2-is-out b/news/coq-85pl2-is-out index 0a5e0caabc..857c218b3b 100644 --- a/news/coq-85pl2-is-out +++ b/news/coq-85pl2-is-out @@ -5,6 +5,6 @@ <#def DESCR> Version 8.5pl2 of Coq is available. It fixes several bugs of version 8.5pl1, including one critical bug. More information can be found in -the CHANGES file. Feedback and +the CHANGES file. Feedback and bug reports are extremely welcome. diff --git a/news/coq-85pl3-is-out b/news/coq-85pl3-is-out index acd3ac8345..e6748aef9f 100644 --- a/news/coq-85pl3-is-out +++ b/news/coq-85pl3-is-out @@ -5,6 +5,6 @@ <#def DESCR> Version 8.5pl3 of Coq is available. It fixes several bugs of version 8.5pl2, including one critical bug. More information can be found in -the CHANGES file. Feedback and +the CHANGES file. Feedback and bug reports are extremely welcome. diff --git a/news/coq-85rc1-is-out b/news/coq-85rc1-is-out index 0643765989..45e2c1a536 100644 --- a/news/coq-85rc1-is-out +++ b/news/coq-85rc1-is-out @@ -23,5 +23,5 @@ testing. The 8.5 version brings several major features to Coq: More information about the changes from 8.4 to 8.5 and since the beta releases can be found in the -CHANGES file. Feedback and +CHANGES file. Feedback and bug reports are extremely welcome. Enjoy! diff --git a/news/coq-86-is-out b/news/coq-86-is-out index 59053eafa9..60277122b3 100644 --- a/news/coq-86-is-out +++ b/news/coq-86-is-out @@ -32,7 +32,7 @@ Coq 8.6 includes:

    More information can be found in the CHANGES file. Feedback and +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6/CHANGES">CHANGES file. Feedback and bug reports are extremely welcome.

    Coq 8.6 initiates a time-based release cycle, with a major version being diff --git a/news/coq-861-is-out b/news/coq-861-is-out index 35f77167c8..3a8b347c73 100644 --- a/news/coq-861-is-out +++ b/news/coq-861-is-out @@ -5,6 +5,6 @@ <#def DESCR> Version 8.6.1 of Coq is available. It fixes several bugs of version 8.6. More information can be found in the CHANGES file. Feedback and +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/CHANGES">CHANGES file. Feedback and bug reports are extremely welcome. diff --git a/news/coq-86beta1-is-out b/news/coq-86beta1-is-out index ccfde92018..7025c9b71e 100644 --- a/news/coq-86beta1-is-out +++ b/news/coq-86beta1-is-out @@ -33,7 +33,7 @@ Coq 8.6 includes:

    More information can be found in the CHANGES file. Feedback and +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6beta1/CHANGES">CHANGES file. Feedback and bug reports are extremely welcome.

    Coq 8.6 initiates a time-based release cycle, with a major version being diff --git a/news/coq-86rc1-is-out b/news/coq-86rc1-is-out index 33c5e37560..67618552f3 100644 --- a/news/coq-86rc1-is-out +++ b/news/coq-86rc1-is-out @@ -33,7 +33,7 @@ Coq 8.6 includes:

    More information can be found in the CHANGES file. Feedback and +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6rc1/CHANGES">CHANGES file. Feedback and bug reports are extremely welcome.

    Coq 8.6 initiates a time-based release cycle, with a major version being diff --git a/news/coq-87beta1-is-out b/news/coq-87beta1-is-out index 3a47f1fd9e..c56db0fe46 100644 --- a/news/coq-87beta1-is-out +++ b/news/coq-87beta1-is-out @@ -35,7 +35,7 @@ Coq 8.7 includes:

    More information can be found in the CHANGES file. Feedback and +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.7+beta1/CHANGES">CHANGES file. Feedback and bug reports are extremely welcome.

    This is the second release of Coq developed on a time-based development diff --git a/pages/coq-82-beta-detailed-description.html b/pages/coq-82-beta-detailed-description.html index d221616cf4..6404171865 100644 --- a/pages/coq-82-beta-detailed-description.html +++ b/pages/coq-82-beta-detailed-description.html @@ -8,7 +8,7 @@

    The support for Haskell-style type classes has been contributed by M. Sozeau and is documented in chapter +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual024.html">chapter 18 of the reference manual.

    The evolutions of the arithmetic libraries cover the following points:

    @@ -32,7 +32,7 @@

    The module +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual007.html">module system has been extended with the include feature, sharing of common submodules, functorial signature application and on-demand parameter inlining (E. Soubiran).

    @@ -40,44 +40,44 @@

    At the level of tactics, Coq 8.2 offers a more efficient implementation of setoid +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual029.html">setoid rewrite, new support for constant unfolding in apply, new dependent +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic84">dependent induction, induction/destruct +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic69">induction/destruct with "in" clause and "e" variants, support for iteration +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic94">iteration and "at" clause in rewrite, new variants of introduction +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual011.html#@tactic82">introduction patterns, support for implicit contents and coercions in the "with" clauses, use of type informations in unification (P. Letouzey, M. Sozeau, S. Glondu, E. Makarov, H. Herbelin). The mathematical proof language is documented in chapter +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual014.html">chapter 11 of the reference manual (P. Corbineau).

    Coq 8.2 also offers miscellaneous syntax extensions and improved -features: destructing let, better type inference, +features: destructing let, better type inference, inference of matching return clause, detection of impossible clause in dependent pattern-matching, detection of decreasing argument in -fixpoints, improved Program and Function -features, new ways to work with implicit arguments, and +fixpoints, improved Program and Function +features, new ways to work with implicit arguments, and various other auxiliary features (M. Sozeau, P. Letouzey, H. Herbelin). It also provides automatic generation of decidable equality (V. Siles).

    Finally, Coq comes with a new stand-alone checker +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/refman/Reference-Manual017.html#toc89">checker for cross-certification of vo-files (B. Barras).

    -

    For all other changes, see the CHANGES file.

    +

    For all other changes, see the CHANGES file.

    As far as we could judge, the major sources of incompatibilities come from the new implementation of setoid rewrite and, marginally, from the support of constant unfolding in apply. A secondary source comes from some bug fixes and from changes in specific libraries. See the COMPATIBILITY file for details and smooth +href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2/COMPATIBILITY">COMPATIBILITY file for details and smooth migration recommendations. We are interested in feedback on the upgrading problems that may be encountered.

    diff --git a/pages/coq-82-beta.html b/pages/coq-82-beta.html index e614301c4a..aa4dd755d3 100644 --- a/pages/coq-82-beta.html +++ b/pages/coq-82-beta.html @@ -9,18 +9,18 @@ evolutions of the arithmetic libraries, and many other various improvements and extensions regarding the module system, tactics, syntax, etc (see the more detailed - description and the summary of + description and the summary of changes).

    We cared for backward compatibility but some specific features may require a few adaptations for upgrading. This is specially the case of (more efficient) setoid rewriting and of the library of functional sets and maps. If you encounter a migration problem not - mentioned in the list of known + mentioned in the list of known incompatibilities, this can be considered as a bug.

    Coq 8.2 is currently released in beta test. We thank beta-tester in advance for feedback on the new version. There is a list of known bugs. + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.2beta4/KNOWN-BUGS">known bugs.

    @@ -37,7 +37,7 @@ - coq-8.2beta4.tar.gz + coq-8.2beta4.tar.gz 4 MB @@ -51,13 +51,13 @@ linuxLinux - + coq-8.2beta4-Linux-i386.tar.gz 24 MB - + coq-8.2beta4-Linux-x86_64.tar.gz 24 MB @@ -67,31 +67,31 @@ redhatRPM - + coq-8.2beta4-1.i386.rpm 24 MB - + coqide-8.2beta4-1.i386.rpm 7 MB - + coq-8.2beta4-1.x86_64.rpm 24 MB - + coqide-8.2beta4-1.x86_64.rpm 5 MB windowsWindows - + coq-8.2beta4-win.exe 80 MB @@ -100,26 +100,26 @@ windowsWindows - + coq-8.2rc2-win.exe 132 MB @@ -97,26 +97,26 @@ ; +
  • a more systematic support for pattern-matching on dependent types;
  • more robust CoqIDE (including a new communication protocol by V. Gross);
    • -
  • a new library of vectors (lists of a given length);
    • +
  • a new library of vectors (lists of a given length);
  • support for referring to expressions of the goal using pattern in tactics;
    • -
  • automatic computation of occurrences to abstract over in destruct/induction (example);
    • -
  • various improvements to Ltac (timeout, appcontext, constr_eq, is_evar, has_evar, generic match _ with _ => _ end pattern, fine-tuning of simpl);
    • +
  • automatic computation of occurrences to abstract over in destruct/induction (example);
    • +
  • various improvements to Ltac (timeout, appcontext, constr_eq, is_evar, has_evar, generic match _ with _ => _ end pattern, fine-tuning of simpl);
  • implicit arguments in anonymous functions;
    • -
  • notations with binders (e.g. exists x y z : A, P x y z) (example);
    • +
  • notations with binders (e.g. exists x y z : A, P x y z) (example);
  • many bug fixes and improvements of existing features (type classes, setoid rewriting, ring, nsatz, micromega, extraction, Function, module system, coq_makefile, ...);

    • For a full log of changes, -see the file +see the file CHANGES.

    -

    Coq 8.4 is not entirely upward compatible with 8.3 (see main incompatibilities)

    +

    Coq 8.4 is not entirely upward compatible with 8.3 (see main incompatibilities)

    - @@ -59,9 +59,9 @@ @@ -74,7 +74,7 @@ alt="macos" />
    MacOS - @@ -100,13 +100,13 @@ - + - @@ -128,7 +128,7 @@

    The development version of Coq is browsable and downloadable from our Git repository using command: git clone git://scm.gforge.inria.fr/coq/coq.git. The daily level of stability of this version (and of the bug-fix branches) can be observed at the coq-bench site or by subscribing to the coq-bench mailing list.

    -

    Most of the previous version of Coq are available here.

    +

    Most of the previous version of Coq are available here.

    diff --git a/pages/coq-85.html b/pages/coq-85.html index a93ca6f962..e73e5fdd31 100644 --- a/pages/coq-85.html +++ b/pages/coq-85.html @@ -40,7 +40,7 @@ terms in Ltac;
  • significant improvements on efficiency in general.
    • -

    For a log of changes, see the file +

    For a log of changes, see the file CHANGES.

    Coq 8.5 is not entirely upward compatible with 8.4

    @@ -49,7 +49,7 @@ - @@ -63,9 +63,9 @@ @@ -79,9 +79,9 @@ @@ -97,7 +97,7 @@ @@ -108,20 +108,20 @@ - + - diff --git a/pages/coq-86.html b/pages/coq-86.html index 2ec5f28e2c..b9a1704c2f 100644 --- a/pages/coq-86.html +++ b/pages/coq-86.html @@ -33,7 +33,7 @@

    A lot of other changes are described in the -CHANGES file.

    +CHANGES file.

    Coq 8.6 initiates a time-based release cycle, with a major version being released every 10 months. @@ -53,7 +53,7 @@

    - @@ -67,7 +67,7 @@ @@ -83,7 +83,7 @@ @@ -101,7 +101,7 @@ @@ -112,15 +112,15 @@ - @@ -134,7 +134,7 @@ @@ -150,7 +150,7 @@ diff --git a/pages/coq-87.html b/pages/coq-87.html index e125da8351..8b42a7e748 100644 --- a/pages/coq-87.html +++ b/pages/coq-87.html @@ -68,7 +68,7 @@ bench-clone-coq site.

    -

    Most of the previous versions of Coq are available here.

    +

    Most of the previous versions of Coq are available here.

    diff --git a/pages/distrib/current/refman/changes.html b/pages/distrib/current/refman/changes.html new file mode 100644 index 0000000000..7f87d51260 --- /dev/null +++ b/pages/distrib/current/refman/changes.html @@ -0,0 +1,4 @@ +<#include "incl/macros.html"> + + + \ No newline at end of file diff --git a/pages/distrib/current/refman/index.html b/pages/distrib/current/refman/index.html new file mode 100644 index 0000000000..0b516e06cf --- /dev/null +++ b/pages/distrib/current/refman/index.html @@ -0,0 +1,4 @@ +<#include "incl/macros.html"> + + + diff --git a/pages/distrib/current/stdlib/index.html b/pages/distrib/current/stdlib/index.html new file mode 100644 index 0000000000..036b9b9def --- /dev/null +++ b/pages/distrib/current/stdlib/index.html @@ -0,0 +1,4 @@ +<#include "incl/macros.html"> + + + diff --git a/pages/download.html b/pages/download.html index 79c4ed8277..8527bdbe41 100644 --- a/pages/download.html +++ b/pages/download.html @@ -80,14 +80,14 @@

    Most previous versions of Coq are available on GitHub -or here.

    +or here.

    diff --git a/pages/v84-0.html b/pages/v84-0.html index eea17124aa..97ab3fbbac 100644 --- a/pages/v84-0.html +++ b/pages/v84-0.html @@ -6,7 +6,7 @@
    -Coq 8.4 is available in beta testing. It features: +Coq 8.4 is available in beta testing. It features:

    For a full log of changes, -see the file +see the file CHANGES.

    Coq 8.4 is not entirely upward compatible with 8.3. Please report manifest regressions not mentioned in the CHANGES file.

    @@ -47,7 +47,7 @@
    - diff --git a/pages/v84.html b/pages/v84.html index eea17124aa..97ab3fbbac 100644 --- a/pages/v84.html +++ b/pages/v84.html @@ -6,7 +6,7 @@
    -Coq 8.4 is available in beta testing. It features: +Coq 8.4 is available in beta testing. It features:

    For a full log of changes, -see the file +see the file CHANGES.

    Coq 8.4 is not entirely upward compatible with 8.3. Please report manifest regressions not mentioned in the CHANGES file.

    @@ -47,7 +47,7 @@
    -
    Sources
    coq-8.4pl6.tar.gz + coq-8.4pl6.tar.gz 4 MB
    + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.4pl6/files/coq-installer-8.4pl6.exe"> coq-installer-8.4pl6.exe (bundled with CoqIDE) - (sha1, sig) + (sha1, sig) 54 MB + coqide-8.4pl5.dmg (bundled with CoqIDE interface)
    Tutorial.pdfTutorial.pdf 0.2 MB
    + Reference-Manual.pdf 1.5 MB
    Sources
    coq-8.5pl3.tar.gz + coq-8.5pl3.tar.gz
    5.2 MB
    + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5pl3/files/coq-installer-8.5pl3-win32.exe"> coq-installer-8.5pl3-win32.exe (32 bits, bundled with CoqIDE, compiled - using CoqSDK) + using CoqSDK) 94 MB + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.5pl3/files/coq-installer-8.5pl3-win64.exe"> coq-installer-8.5pl3-win64.exe (64 bits, bundled with CoqIDE, compiled - using CoqSDK 64 bits) + using CoqSDK 64 bits) 92 MB - + CoqIDE_8.5pl3.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14)
    Tutorial.pdfTutorial.pdf 0.2 MB
    - Reference-Manual.pdf (also online) + + Reference-Manual.pdf (also online) 1.6 MB
    - Standard Library online documentation + Standard Library online documentation
    Sources
    coq-8.6.1.tar.gz + coq-8.6.1.tar.gz
    5.3 MB
    + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/files/coq-installer-8.6.1-i686.exe"> coq-installer-8.6.1-i686.exe (32 bits, bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14) + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/files/coq-installer-8.6.1-x86_64.exe"> coq-installer-8.6.1-x86_64.exe (64 bits, bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14) - + CoqIDE_8.6.1.dmg (bundled with CoqIDE, compiled using OCaml 4.02.3 and Camlp5 6.14)
    - Reference-Manual.pdf (also online) + + Reference-Manual.pdf (also online) 1.7 MB
    - Standard Library online documentation + Standard Library online documentation
    + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/files/coq-opensource-archive-i686.zip"> coq-opensource-archive-i686.zip (sources of the files installed by the 32 bit Windows installer, to comply with license requirements) + href="https://coq-distrib.s3-website.fr-par.scw.cloud/V8.6.1/files/coq-opensource-archive-x86_64.zip"> coq-opensource-archive-x86_64.zip (sources of the files installed by the 64 bit Windows installer, to comply with license requirements)
    Sources
    coq-8.4beta.tar.gz + coq-8.4beta.tar.gz 3.7 MB
    Sources
    coq-8.4beta.tar.gz + coq-8.4beta.tar.gz 3.7 MB