From 4b4a4b6b41e6b303d556638ed2a79b1493b1ecf4 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 13 Jan 2016 17:38:27 +0100 Subject: MMaps: remove it from final 8.5 release, since this new library isn't mature enough In particular, its interface might still change (in interaction with interested colleagues). So let's not give it too much visibility yet. Instead, I'll turn it as an opam packages for now. --- doc/stdlib/index-list.html.template | 7 ------- 1 file changed, 7 deletions(-) (limited to 'doc') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 292b2b36cc..d6b1af797f 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -476,13 +476,6 @@ through the Require Import command.

theories/MSets/MSetPositive.v theories/MSets/MSetToFiniteSet.v (theories/MSets/MSets.v) - theories/MMaps/MMapAVL.v - theories/MMaps/MMapFacts.v - theories/MMaps/MMapInterface.v - theories/MMaps/MMapList.v - theories/MMaps/MMapPositive.v - theories/MMaps/MMapWeakList.v - (theories/MMaps/MMaps.v)
FSets: -- cgit v1.2.3 From 13e969e644a6ad23f6d326f3e4a253ae0393da9c Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 15 Jan 2016 20:29:41 +0100 Subject: Thanks Hugo, but let's remain factual. --- doc/refman/RefMan-pre.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index e0dc496666..cb2ab5dc2f 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1080,8 +1080,7 @@ Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc, Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François -Ripault, Carst Tankink. Maxime Dénès brilliantly coordinated the -release process. +Ripault, Carst Tankink. Maxime Dénès coordinated the release process. \begin{flushright} Paris, January 2015, revised December 2015,\\ -- cgit v1.2.3 From 281e4cb8b04c7fd13ec6416e4dcd05ffa1f48761 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Jan 2016 16:56:11 +0100 Subject: Clarifying the documentation of tactics "cbv" and "lazy". Following a discussion on coq-club on Jan 13, 2016. --- doc/refman/RefMan-tac.tex | 40 +++++++++++++++++++++++++--------------- 1 file changed, 25 insertions(+), 15 deletions(-) (limited to 'doc') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b3a730e675..9a365b8297 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3047,23 +3047,33 @@ variables bound by a let-in construction inside the term itself (use here the {\tt zeta} flag). In any cases, opaque constants are not unfolded (see Section~\ref{Opaque}). -The goal may be normalized with two strategies: {\em lazy} ({\tt lazy} -tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy -is a call-by-need strategy, with sharing of reductions: the arguments of a -function call are partially evaluated only when necessary, and if an -argument is used several times then it is computed only once. This -reduction is efficient for reducing expressions with dead code. For -instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a -pair of a witness $t$, and a proof that $t$ satisfies the predicate -$P$. Most of the time, $t$ may be computed without computing the proof -of $P(t)$, thanks to the lazy strategy. +Normalization according to the flags is done by first evaluating the +head of the expression into a {\em weak-head} normal form, i.e. until +the evaluation is bloked by a variable (or an opaque constant, or an +axiom), as e.g. in {\tt x\;u$_1$\;...\;u$_n$}, or {\tt match x with + ... end}, or {\tt (fix f x \{struct x\} := ...) x}, or is a +constructed form (a $\lambda$-expression, a constructor, a cofixpoint, +an inductive type, a product type, a sort), or is a redex that the +flags prevent to reduce. Once a weak-head normal form is obtained, +subterms are recursively reduced using the same strategy. + +Reduction to weak-head normal form can be done using two strategies: +{\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv} +tactic). The lazy strategy is a call-by-need strategy, with sharing of +reductions: the arguments of a function call are weakly evaluated only +when necessary, and if an argument is used several times then it is +weakly computed only once. This reduction is efficient for reducing +expressions with dead code. For instance, the proofs of a proposition +{\tt exists~$x$. $P(x)$} reduce to a pair of a witness $t$, and a +proof that $t$ satisfies the predicate $P$. Most of the time, $t$ may +be computed without computing the proof of $P(t)$, thanks to the lazy +strategy. The call-by-value strategy is the one used in ML languages: the -arguments of a function call are evaluated first, using a weak -reduction (no reduction under the $\lambda$-abstractions). Despite the -lazy strategy always performs fewer reductions than the call-by-value -strategy, the latter is generally more efficient for evaluating purely -computational expressions (i.e. with few dead code). +arguments of a function call are systematically weakly evaluated +first. Despite the lazy strategy always performs fewer reductions than +the call-by-value strategy, the latter is generally more efficient for +evaluating purely computational expressions (i.e. with few dead code). \begin{Variants} \item {\tt compute} \tacindex{compute}\\ -- cgit v1.2.3 From 1af878e0dac2198ae487d0b37438520772f28350 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Jan 2016 17:07:32 +0100 Subject: Documenting Set Bullet Behavior. This is useful for restoring bullets after e.g. loading ssreflect. Hoping Arnaud is ok in documenting it. --- doc/refman/RefMan-pro.tex | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'doc') diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index ed1b79e56e..c37367de5b 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -407,6 +407,19 @@ Proof. \end{ErrMsgs} +The bullet behavior can be controlled by the following commands. + +\begin{quote} +Set Bullet Behavior "None". +\end{quote} + +This makes bullets inactive. + +\begin{quote} +Set Bullet Behavior "Strict Subproofs". +\end{quote} + +This makes bullets active (this is the default behavior). \section{Requesting information} -- cgit v1.2.3 From af5eafaee218935c35f0bd906727d2d2370bd136 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 15:57:24 +0100 Subject: Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500. --- doc/refman/RefMan-ext.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index f2ab79dced..51e881bff4 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -2014,7 +2014,7 @@ variables, use Instead of letting the unification engine try to solve an existential variable by itself, one can also provide an explicit hole together with a tactic to solve -it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a +it. Using the syntax {\tt ltac:(\expr)}, the user can put a tactic anywhere a term is expected. The order of resolution is not specified and is implementation-dependent. The inner tactic may use any variable defined in its scope, including repeated alternations between variables introduced by term -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- doc/common/styles/html/coqremote/cover.html | 2 +- doc/common/styles/html/simple/cover.html | 2 +- doc/common/title.tex | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index db82717094..6ec4dc1af0 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -60,7 +60,7 @@
  • V8.2 © INRIA 2008-2011
  • V8.3 © INRIA 2010-2011
  • V8.4 © INRIA 2012-2014
    • -
  • V8.5 © INRIA 2015
    • +
  • V8.5 © INRIA 2015-2016

    • This research was partly supported by IST diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 1641a1ed37..328bd68daf 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -38,7 +38,7 @@

  • V8.2 © INRIA 2008-2011
  • V8.3 © INRIA 2010-2011
  • V8.4 © INRIA 2012-2014
    • -
  • V8.5 © INRIA 2015
    • +
  • V8.5 © INRIA 2015-2016

    • This research was partly supported by IST diff --git a/doc/common/title.tex b/doc/common/title.tex index 4716c3156a..0e072b6b65 100644 --- a/doc/common/title.tex +++ b/doc/common/title.tex @@ -45,7 +45,7 @@ V\coqversion, \today %END LATEX \copyright INRIA 1999-2004 ({\Coq} versions 7.x) -\copyright INRIA 2004-2015 ({\Coq} versions 8.x) +\copyright INRIA 2004-2016 ({\Coq} versions 8.x) #3 \end{flushleft} -- cgit v1.2.3