From 29ff821da57e35d37b41be34febb275306c4809f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 5 Nov 2016 11:33:42 +0100 Subject: Minor fix in documentation --- doc/refman/RefMan-tac.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 656ae57b95..54393e46f6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1278,7 +1278,7 @@ in the list of subgoals remaining to prove. In particular, \texttt{pose proof {\term} as {\ident}} behaves as \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term} - as {\intropattern}\tacindex{pose proof}} is the same as applying + as {\intropattern}} is the same as applying the {\intropattern} to {\term}. \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough} -- cgit v1.2.3 From d6edca2f025574fd84ef7e37a178c42674ff5840 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 5 Nov 2016 11:34:10 +0100 Subject: Credits for 8.6 --- doc/refman/RefMan-pre.tex | 129 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 129 insertions(+) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index cb2ab5dc2f..c7a3c7415a 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1087,6 +1087,135 @@ Paris, January 2015, revised December 2015,\\ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\ \end{flushright} +\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)} + +{\Coq} version 8.6 contains the result of refinements, stabilization of +8.5's features and cleanups of the internals of the system. Over the +year of (now time-based) development, about 450 bugs were resolved and +over 100 contributions integrated. The main user visible changes are: +\begin{itemize} +\item A new, state-of-the-art universe constraint checker that + can outperform the previous version by an order of magnitude, by + Jacques-Henri Jourdan. +\item In CoqIDE and other asynchronous interfaces, more fine-grained + asynchronous processing and error reporting by Enrico Tassi. +\item More access to the proof engine features from Ltac: goal + management primitives, range selectors and a {\tt typeclasses + eauto} engine handling multiple goals and multiple successes, by + Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. +\item Tactic behavior uniformization and specification, generalization + of intro-patterns by Hugo Herbelin and others. +\item Update of the beautifier by Hugo Herbelin, useful for switching + between versions. +\item A brand new warning system allowing to control warnings, turn them + into errors or ignore them selectively by Maxime Dénès, Guillaume + Melquiond and others. +\item Irrefutable patterns in abstractions, by Daniel de Rauglaudre. +\item Integration of {\tt ssreflect}'s subterm selection algorithm by + Enrico Tassi. +\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Tobias + Tebbi, Jason Gross and Paul Steckler. +\end{itemize} + +{\Coq} 8.6 also comes with a bunch of smaller-scale changes and +improvements regarding the different components of the system. We shall +only list a few of them. + +The {\tt iota} reduction flag is now a shorthand for {\tt match}, {\tt + fix} and {\tt cofix} flags controlling the corresponding reduction +rules (by Hugo Herbelin and Maxime Dénès). + +Maxime Dénès maintained the native compilation machinery. + +Pierre-Marie Pédrot separated the Ltac code from general purpose +tactics, and generalized and rationalized the handling of generic +arguments, allowing to create new versions of Ltac more easily in the +future. + +Many tactics have now more uniform behavior w.r.t. intro-patterns thanks +to Hugo Herbelin who also improved the basic tactics here and there. + +In patterns and terms, {\tt @}, abbreviations and notations are now +interpreted the same way, by Hugo Herbelin. + +Name handling for universes has been improved by Pierre-Marie Pédrot and +Matthieu Sozeau. The minimization algorithm has been improved by +Matthieu Sozeau. + +The unifier has been improved by Hugo Herbelin and Matthieu Sozeau, +fixing some incompatibilities introduced in Coq 8.5. Unification +constraints can now be left floating around and be seen by the user +thanks to a new option. The {\tt Keyed Unification} mode has been +improved by Matthieu Sozeau. + +The typeclass resolution engine and associated proof-search tactic have +been reimplemented on top of the proof-engine monad, providing better +integration in tactics, and new options have been introduced to control +it, by Matthieu Sozeau with help from Théo Zimmermann. + +The efficiency of the whole system has been significantly improved +thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and +Matthieu Sozeau and performance issue tracking by Jason Gross and Paul +Steckler. + +Standard library improvements by Jason Gross, Sébastien Hinderer, Pierre +Letouzey and others. + +Emilio Jesús Gallego Arias contributed many cleanups and refactorings of +the pretty-printing and user interface communication components. + +Frédéric Besson maintained the micromega tactic. + +The OPAM repository for {\Coq} packages has been maintained by Guillaume +Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A +list of packages is now available at \url{https://coq.inria.fr/opam/www/}. + +Packaging tools were provided by Michael Soegtrop and Enrico Tassi +(Windows), Maxime Dénès and Matthieu Sozeau (MacOS X). Packages are now +regularly built on the continuous integration server. + +Matej Košík maintained and greatly improved the continuous integration +setup and the testing of {\Coq} contributions. He also contributed many +API improvement and code cleanups throughout the system. + +Many power users helped to improve the design of the new features via +the bug tracker, the pull request system, the {\Coq} development mailing +list or the coq-club mailing list. Special thanks to the users who +contributed patches and intensive brain-storming and code reviews, +starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan +Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel +Sherer and Beta Ziliani. It would however be impossible to mention with +precision all the names of people who to some extent influenced the +development. + +Version 8.6 is the first release of {\Coq} developed on a time-based +development cycle. Its development spanned 10 months from the release of +{\Coq} 8.5 and was based on a public roadmap. To date, it contains more +external contributions than any previous {\Coq} system. Code reviews +were systematically done before integration of new features, with an +important focus given to compatibility and performance issues, resulting +in a much more robust release than previous ones. + +General maintenance during part or whole of this period has been done by +Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre +Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, +Arnaud Spiwack, Enrico Tassi as well as Bruno Barras, Yves Bertot, +Frédéric Besson, Assia Mahboubi, Yann Régis-Gianas. The development +process was coordinated by Matthieu Sozeau with the help of Maxime +Dénès, who was also in charge of the release process. + +Coq Enhancement Proposals (CEPs for short) were introduced by Enrico +Tassi to provide more visibility and a discussion period on new +features, they are publicly available \url{https://github.com/coq/ceps}. + +Started during this period, an effort is led by Yves Bertot and Maxime +Dénès to put together a {\Coq} consortium. + +\begin{flushright} +Paris, November 2016,\\ +Matthieu Sozeau and the {\Coq} development team\\ +\end{flushright} + %new Makefile -- cgit v1.2.3 From 25fc9919c6d86fa8119b1f0c8e5ddba156055c9d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 6 Nov 2016 08:54:37 +0100 Subject: Fixes from Enrico's review --- doc/refman/RefMan-pre.tex | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index c7a3c7415a..669ba11e81 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1113,8 +1113,8 @@ over 100 contributions integrated. The main user visible changes are: \item Irrefutable patterns in abstractions, by Daniel de Rauglaudre. \item Integration of {\tt ssreflect}'s subterm selection algorithm by Enrico Tassi. -\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Tobias - Tebbi, Jason Gross and Paul Steckler. +\item Integration of {\tt LtacProf}, a profiler for {\tt Ltac} by Jason + Gross, Paul Steckler, Enrico Tassi and Tobias Tebbi. \end{itemize} {\Coq} 8.6 also comes with a bunch of smaller-scale changes and @@ -1170,14 +1170,23 @@ The OPAM repository for {\Coq} packages has been maintained by Guillaume Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A list of packages is now available at \url{https://coq.inria.fr/opam/www/}. -Packaging tools were provided by Michael Soegtrop and Enrico Tassi -(Windows), Maxime Dénès and Matthieu Sozeau (MacOS X). Packages are now -regularly built on the continuous integration server. +Packaging tools and software development kits were prepared by Maxime +Dénès, Michael Soegtrop and Enrico Tassi for Windows, and Maxime Dénès +and Matthieu Sozeau for MacOS X. Packages are now regularly built on the +continuous integration server. Matej Košík maintained and greatly improved the continuous integration setup and the testing of {\Coq} contributions. He also contributed many API improvement and code cleanups throughout the system. +General maintenance during part or whole of this period has been done by +Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre +Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, +Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot, +Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development +process was coordinated by Matthieu Sozeau with the help of Maxime +Dénès, who was also in charge of the release process. + Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the {\Coq} development mailing list or the coq-club mailing list. Special thanks to the users who @@ -1194,15 +1203,7 @@ development cycle. Its development spanned 10 months from the release of external contributions than any previous {\Coq} system. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues, resulting -in a much more robust release than previous ones. - -General maintenance during part or whole of this period has been done by -Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre -Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, -Arnaud Spiwack, Enrico Tassi as well as Bruno Barras, Yves Bertot, -Frédéric Besson, Assia Mahboubi, Yann Régis-Gianas. The development -process was coordinated by Matthieu Sozeau with the help of Maxime -Dénès, who was also in charge of the release process. +in a hopefully much more robust release than previous ones. Coq Enhancement Proposals (CEPs for short) were introduced by Enrico Tassi to provide more visibility and a discussion period on new -- cgit v1.2.3 From ceaafcde70e0ba536cae03baa740563aff47f6e8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 6 Nov 2016 11:22:31 +0100 Subject: Maxime's comments --- doc/refman/RefMan-pre.tex | 36 ++++++++++++++++++++---------------- 1 file changed, 20 insertions(+), 16 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 669ba11e81..944cd48481 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1087,7 +1087,7 @@ Paris, January 2015, revised December 2015,\\ Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\ \end{flushright} -\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)} +\section*{Credits: version 8.6} {\Coq} version 8.6 contains the result of refinements, stabilization of 8.5's features and cleanups of the internals of the system. Over the @@ -1098,7 +1098,8 @@ over 100 contributions integrated. The main user visible changes are: can outperform the previous version by an order of magnitude, by Jacques-Henri Jourdan. \item In CoqIDE and other asynchronous interfaces, more fine-grained - asynchronous processing and error reporting by Enrico Tassi. + asynchronous processing and error reporting by Enrico Tassi (ability + to jump to any error in the document). \item More access to the proof engine features from Ltac: goal management primitives, range selectors and a {\tt typeclasses eauto} engine handling multiple goals and multiple successes, by @@ -1170,22 +1171,25 @@ The OPAM repository for {\Coq} packages has been maintained by Guillaume Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A list of packages is now available at \url{https://coq.inria.fr/opam/www/}. -Packaging tools and software development kits were prepared by Maxime -Dénès, Michael Soegtrop and Enrico Tassi for Windows, and Maxime Dénès -and Matthieu Sozeau for MacOS X. Packages are now regularly built on the -continuous integration server. +Packaging tools and software development kits were prepared by Michael +Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and +Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly +built on the continuous integration server. Matej Košík maintained and greatly improved the continuous integration setup and the testing of {\Coq} contributions. He also contributed many API improvement and code cleanups throughout the system. -General maintenance during part or whole of this period has been done by -Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre -Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau, -Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot, -Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development -process was coordinated by Matthieu Sozeau with the help of Maxime -Dénès, who was also in charge of the release process. +The contributors for this version are C.J. Bell, Yves Bertot, Frédéric +Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason +Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, +Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien +Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot, +Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul +Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo +Zimmermann and Daniel de Rauglaudre. The development process was +coordinated by Hugo Herbelin and Matthieu Sozeau with the help of +Maxime Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the {\Coq} development mailing @@ -1193,8 +1197,8 @@ list or the coq-club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel -Sherer and Beta Ziliani. It would however be impossible to mention with -precision all the names of people who to some extent influenced the +Sherer and Beta Ziliani. It would however be impossible to mention +exhaustively the names of everybody who to some extent influenced the development. Version 8.6 is the first release of {\Coq} developed on a time-based @@ -1203,7 +1207,7 @@ development cycle. Its development spanned 10 months from the release of external contributions than any previous {\Coq} system. Code reviews were systematically done before integration of new features, with an important focus given to compatibility and performance issues, resulting -in a hopefully much more robust release than previous ones. +in a hopefully more robust release than {\Coq} 8.5. Coq Enhancement Proposals (CEPs for short) were introduced by Enrico Tassi to provide more visibility and a discussion period on new -- cgit v1.2.3 From bf8827788d1d8c0dc96b963d3c35985d8b3725c6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 6 Nov 2016 11:48:06 +0100 Subject: Hugo's comments --- doc/refman/RefMan-pre.tex | 2 -- 1 file changed, 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 944cd48481..6ba2f850ee 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1106,8 +1106,6 @@ over 100 contributions integrated. The main user visible changes are: Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. \item Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others. -\item Update of the beautifier by Hugo Herbelin, useful for switching - between versions. \item A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond and others. -- cgit v1.2.3 From a96fed4624d8baaa4bec9bb63676eb1bcb389091 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Nov 2016 09:36:30 +0100 Subject: Hugo and Maxime's 2nd pass of comments --- doc/refman/RefMan-pre.tex | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 6ba2f850ee..29ae51fea5 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1108,7 +1108,7 @@ over 100 contributions integrated. The main user visible changes are: of intro-patterns by Hugo Herbelin and others. \item A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume - Melquiond and others. + Melquiond, Pierre-Marie Pédrot and others. \item Irrefutable patterns in abstractions, by Daniel de Rauglaudre. \item Integration of {\tt ssreflect}'s subterm selection algorithm by Enrico Tassi. @@ -1131,9 +1131,6 @@ tactics, and generalized and rationalized the handling of generic arguments, allowing to create new versions of Ltac more easily in the future. -Many tactics have now more uniform behavior w.r.t. intro-patterns thanks -to Hugo Herbelin who also improved the basic tactics here and there. - In patterns and terms, {\tt @}, abbreviations and notations are now interpreted the same way, by Hugo Herbelin. @@ -1179,15 +1176,16 @@ setup and the testing of {\Coq} contributions. He also contributed many API improvement and code cleanups throughout the system. The contributors for this version are C.J. Bell, Yves Bertot, Frédéric -Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason -Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan, -Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien -Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot, -Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul -Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo -Zimmermann and Daniel de Rauglaudre. The development process was -coordinated by Hugo Herbelin and Matthieu Sozeau with the help of -Maxime Dénès, who was also in charge of the release process. +Besson, Pierre Boutillier, Tej Chajed, Pierre Courtieu, Maxime Dénès, +Ricky Elrod, Jason Gross, Hugo Herbelin, Sébastien Hinderer, Emilio +Jesus Gallego Arias, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy, +Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, +Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Daniel de +Rauglaudre, Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud +Spiwack, Paul Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich +and Théo Zimmermann. The development process was coordinated by Hugo +Herbelin and Matthieu Sozeau with the help of Maxime Dénès, who was also +in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the {\Coq} development mailing @@ -1195,7 +1193,7 @@ list or the coq-club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel -Sherer and Beta Ziliani. It would however be impossible to mention +Scherer and Beta Ziliani. It would however be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -- cgit v1.2.3 From 1692b9e8245fbf485c40c9b6dd311f124978e987 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Nov 2016 13:49:57 +0100 Subject: More accurate contributor list. Command used: git log v8.5..HEAD --pretty=format:"%an," | sort -k 2 | uniq with some manual postprocessing for login names, particles and multiple first names. --- doc/refman/RefMan-pre.tex | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 29ae51fea5..4578bee120 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1175,24 +1175,25 @@ Matej Košík maintained and greatly improved the continuous integration setup and the testing of {\Coq} contributions. He also contributed many API improvement and code cleanups throughout the system. -The contributors for this version are C.J. Bell, Yves Bertot, Frédéric -Besson, Pierre Boutillier, Tej Chajed, Pierre Courtieu, Maxime Dénès, -Ricky Elrod, Jason Gross, Hugo Herbelin, Sébastien Hinderer, Emilio -Jesus Gallego Arias, Jacques-Henri Jourdan, Matej Košík, Xavier Leroy, +The contributors for this version are Bruno Barras, C.J. Bell, Yves +Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume +Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Ricky Elrod, Emilio Jesus Gallego Arias, Jason Gross, Hugo Herbelin, +Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, -Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, Daniel de -Rauglaudre, Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud -Spiwack, Paul Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich -and Théo Zimmermann. The development process was coordinated by Hugo -Herbelin and Matthieu Sozeau with the help of Maxime Dénès, who was also -in charge of the release process. +Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel +de Rauglaudre, Lionel Rieg, Gabriel Scherer, Thomas Sibut-Pinote, +Matthieu Sozeau, Arnaud Spiwack, Paul Steckler, Enrico Tassi, Laurent +Théry, Nickolai Zeldovich and Théo Zimmermann. The development process +was coordinated by Hugo Herbelin and Matthieu Sozeau with the help of +Maxime Dénès, who was also in charge of the release process. Many power users helped to improve the design of the new features via the bug tracker, the pull request system, the {\Coq} development mailing list or the coq-club mailing list. Special thanks to the users who contributed patches and intensive brain-storming and code reviews, starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan -Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel +Leivent, Xavier Leroy, Gregory Malecha, Clément Pit--Claudel, Gabriel Scherer and Beta Ziliani. It would however be impossible to mention exhaustively the names of everybody who to some extent influenced the development. -- cgit v1.2.3 From 3bc8d841148da0cf1db5b9b896f28c3285d4f5db Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 7 Nov 2016 17:31:48 +0100 Subject: After Emilio's comment. --- doc/refman/RefMan-pre.tex | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 4578bee120..8f75353bb3 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1169,7 +1169,9 @@ list of packages is now available at \url{https://coq.inria.fr/opam/www/}. Packaging tools and software development kits were prepared by Michael Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and Maxime Dénès and Matthieu Sozeau for MacOS X. Packages are now regularly -built on the continuous integration server. +built on the continuous integration server. {\Coq} now comes with a {\tt + META} file usable with {\tt ocamlfind}, contributed by Emilio Jesús +Gallego Arias, Gregory Malecha, and Matthieu Sozeau. Matej Košík maintained and greatly improved the continuous integration setup and the testing of {\Coq} contributions. He also contributed many @@ -1178,7 +1180,7 @@ API improvement and code cleanups throughout the system. The contributors for this version are Bruno Barras, C.J. Bell, Yves Bertot, Frédéric Besson, Pierre Boutillier, Tej Chajed, Guillaume Claret, Xavier Clerc, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, -Ricky Elrod, Emilio Jesus Gallego Arias, Jason Gross, Hugo Herbelin, +Ricky Elrod, Emilio Jesús Gallego Arias, Jason Gross, Hugo Herbelin, Sébastien Hinderer, Jacques-Henri Jourdan, Matej Kosik, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien Mangin, Erik Martin-Dorel, Guillaume Melquiond, Clément Pit--Claudel, Pierre-Marie Pédrot, Daniel -- cgit v1.2.3 From cadb9e6614a1e72bf18f80acf0aabaeed4e9f057 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 8 Nov 2016 09:00:13 +0100 Subject: Rewording from Enrico --- doc/refman/RefMan-pre.tex | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 8f75353bb3..4f4f404422 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1098,8 +1098,9 @@ over 100 contributions integrated. The main user visible changes are: can outperform the previous version by an order of magnitude, by Jacques-Henri Jourdan. \item In CoqIDE and other asynchronous interfaces, more fine-grained - asynchronous processing and error reporting by Enrico Tassi (ability - to jump to any error in the document). + asynchronous processing and error reporting by Enrico Tassi. In + asynchronous mode {\Coq} is now capable of recovering from errors + and continue processing the document. \item More access to the proof engine features from Ltac: goal management primitives, range selectors and a {\tt typeclasses eauto} engine handling multiple goals and multiple successes, by -- cgit v1.2.3