From 2ddc9d12bd4616f10245c40bc0c87ae548911809 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 19:13:58 +0200
Subject: Fixing #5420 as well as many related bugs due to miscounting let-ins.

- Supporting let-ins in tactic "fix", and hence in interactive
  Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
  presence of let-ins.
---
 doc/refman/RefMan-tac.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3f12411863..0edc66f839 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2618,9 +2618,9 @@ as the ones described in Section~\ref{Tac-induction}.
 In the syntax of the tactic, the identifier {\ident} is the name given
 to the induction hypothesis. The natural number {\num} tells on which
 premise of the current goal the induction acts, starting
-from 1 and counting both dependent and non dependent
-products. Especially, the current lemma must be composed of at least
-{\num} products.
+from 1, counting both dependent and non dependent
+products, but skipping local definitions. Especially, the current
+lemma must be composed of at least {\num} products.
 
 Like in a {\tt fix} expression, the induction
 hypotheses have to be used on structurally smaller arguments.
-- 
cgit v1.2.3


From 41b3486501f0217f0b0c552f21d6f0374b55a3ba Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 28 Jan 2017 14:02:02 +0100
Subject: Mention template polymorphism in the documentation.

Since About mentions it the doc should as well.
---
 doc/refman/RefMan-cic.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index b9c17d8148..12f390e44f 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1120,6 +1120,12 @@ Check (fun (A:Prop) (B:Set) => prod A B).
 Check (fun (A:Type) (B:Prop) => prod A B).
 \end{coq_example}
 
+Internally, Coq calls sort polymorphism of inductive types
+{\em template polymorphism}. For instance:
+\begin{coq_example}
+About prod.
+\end{coq_example}
+
 \subsection{Destructors}
 The specification of inductive definitions with arities and
 constructors is quite natural.  But we still have to say how to use an
-- 
cgit v1.2.3


From d3a2acc9fceff7476bc2d9eaadab8411365172a2 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 31 Mar 2017 15:03:34 +0200
Subject: Use "template polymorphism" in the documentation.

---
 doc/refman/RefMan-cic.tex | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 12f390e44f..e26d4b18da 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified
 identifier with a number) or a successor of an algebraic universe (an
 expression $u+1$), or an upper bound of algebraic universes (an
 expression $max(u_1,...,u_n)$), or the base universe (the expression
-$0$) which corresponds, in the arity of sort-polymorphic inductive
-types (see Section \ref{Sort-polymorphism-inductive}),
+$0$) which corresponds, in the arity of template polymorphic inductive
+types (see Section \ref{Template-polymorphism}),
 to the predicative sort {\Set}. A graph of constraints between
 the universe variables is maintained globally. To ensure the existence
 of a mapping of the universes to the positive integers, the graph of
@@ -977,8 +977,8 @@ Inductive exType (P:Type->Prop) : Type :=
 %is recursive or not.  We shall write the type $(x:_R T)C$ if it is 
 %a recursive argument and $(x:_P T)C$ if the argument is not recursive.
 
-\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}}
-\label{Sort-polymorphism-inductive}
+\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}}
+\label{Template-polymorphism}
 
 Inductive types declared in {\Type} are
 polymorphic over their arguments in {\Type}.
@@ -1120,12 +1120,6 @@ Check (fun (A:Prop) (B:Set) => prod A B).
 Check (fun (A:Type) (B:Prop) => prod A B).
 \end{coq_example}
 
-Internally, Coq calls sort polymorphism of inductive types
-{\em template polymorphism}. For instance:
-\begin{coq_example}
-About prod.
-\end{coq_example}
-
 \subsection{Destructors}
 The specification of inductive definitions with arities and
 constructors is quite natural.  But we still have to say how to use an
-- 
cgit v1.2.3


From d70af8a387d1199be3327b3e4ef21dda9bb2155e Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 11 Apr 2017 12:47:29 +0200
Subject: Update RefMan-pre to mention template polymorphism.

---
 doc/refman/RefMan-pre.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index f36969e821..0441f952df 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -529,7 +529,7 @@ intensive computations.
 
 Christine Paulin implemented an extension of inductive types allowing
 recursively non uniform parameters. Hugo Herbelin implemented
-sort-polymorphism for inductive types.
+sort-polymorphism for inductive types (now called template polymorphism).
 
 Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary
 compatible equivalence relations. He also generalized rewriting to
-- 
cgit v1.2.3


From 15d415729962eddde2cd1d58e03449c8526ba626 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 24 Apr 2017 16:39:25 +0200
Subject: refman: remember the old name of template polymorphism.

---
 doc/refman/RefMan-cic.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index e26d4b18da..fdd2725810 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1120,6 +1120,10 @@ Check (fun (A:Prop) (B:Set) => prod A B).
 Check (fun (A:Type) (B:Prop) => prod A B).
 \end{coq_example}
 
+\Rem Template polymorphism used to be called ``sort-polymorphism of
+inductive types'' before universe polymorphism (see
+Chapter~\ref{Universes-full}) was introduced.
+
 \subsection{Destructors}
 The specification of inductive definitions with arities and
 constructors is quite natural.  But we still have to say how to use an
-- 
cgit v1.2.3


From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 doc/refman/RefMan-ltac.tex | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 9378529cbe..46274e12f3 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1087,8 +1087,8 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting}
-\index{Tacticals!abstract@{\tt abstract}}}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\tacindex{transparent\_abstract}\comindex{Qed exporting}
+\index{Tacticals!abstract@{\tt abstract}}\index{Tacticals!transparent\_abstract@{\tt transparent\_abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
@@ -1114,13 +1114,17 @@ on. This can be obtained thanks to the option below.
 {\tt Set Shrink Abstract}
 \end{quote}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}} are
-quantified only over the variables that appear in the term constructed by
-\texttt{\tacexpr}.
+When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
+variables that appear in the term constructed by \texttt{\tacexpr}.
 
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
+\item \texttt{transparent\_abstract {\tacexpr}}.\\
+  Save the subproof in a transparent lemma rather than an opaque one.
+\item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
+  Give explicitly the name of the auxiliary transparent lemma.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}
-- 
cgit v1.2.3


From 84845f766d9b9d532f615352fbc8a0e78e1727e9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Mon, 27 Mar 2017 13:28:17 -0400
Subject: Mark transparent_abstract as risky in docs

As per Enrico's request.
---
 doc/refman/RefMan-ltac.tex | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 46274e12f3..c2f52e23bc 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1121,10 +1121,17 @@ variables that appear in the term constructed by \texttt{\tacexpr}.
 \begin{Variants}
 \item \texttt{abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary lemma.
+  Use this feature at your own risk; explicitly named and reused subterms
+  don't play well with asynchronous proofs.
 \item \texttt{transparent\_abstract {\tacexpr}}.\\
   Save the subproof in a transparent lemma rather than an opaque one.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile.
 \item \texttt{transparent\_abstract {\tacexpr} using {\ident}}.\\
   Give explicitly the name of the auxiliary transparent lemma.
+  Use this feature at your own risk; building computationally relevant terms
+  with tactics is fragile, and explicitly named and reused subterms
+  don't play well with asynchronous proofs.
 \end{Variants}
 
 \ErrMsg \errindex{Proof is not complete}
-- 
cgit v1.2.3


From e574b4bdd974daa7d2ceecf799762be92fadff44 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Thu, 27 Apr 2017 12:05:51 -0400
Subject: fix order of command-line arguments mentioned in Add LoadPath

---
 doc/refman/RefMan-oth.tex | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 56ce753cd6..a25da7d926 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -697,8 +697,8 @@ which can be any valid path.
 
 \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
 
-This command is equivalent to the command line option {\tt -Q {\dirpath}
-  {\str}}. It adds the physical directory {\str} to the current {\Coq}
+This command is equivalent to the command line option {\tt -Q {\str}
+  {\dirpath}}. It adds the physical directory {\str} to the current {\Coq}
 loadpath and maps it to the logical directory {\dirpath}.
 
 \begin{Variants}
@@ -707,8 +707,8 @@ Performs as {\tt Add LoadPath {\str} as {\dirpath}} but for the empty directory
 \end{Variants}
 
 \subsection[\tt Add Rec LoadPath {\str} as {\dirpath}.]{\tt Add Rec LoadPath {\str} as {\dirpath}.\comindex{Add Rec LoadPath}\label{AddRecLoadPath}}
-This command is equivalent to the command line option {\tt -R {\dirpath}
-  {\str}}. It adds the physical directory {\str} and all its
+This command is equivalent to the command line option {\tt -R {\str}
+  {\dirpath}}. It adds the physical directory {\str} and all its
 subdirectories to the current {\Coq} loadpath.
 
 \begin{Variants}
-- 
cgit v1.2.3


From 5365971dfdf4136586527aa4f4c85fbfebeee0bd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 15:00:56 +0200
Subject: Fix for bug 5507. Mispelt de Bruijn.

---
 doc/refman/RefMan-tus.tex | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 797b0adedd..c55b3775cf 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -299,7 +299,7 @@ vector of terms $vt$.
 \end{itemize}
 
 In this meta-language, bound variables are represented using the
-so-called deBrujin's indexes. In this representation, an occurrence of
+so-called deBruijn's indexes. In this representation, an occurrence of
 a bound variable is denoted by an integer, meaning the number of
 binders that must be traversed to reach its own
 binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
@@ -482,7 +482,7 @@ following constructor functions:
 
 \begin{description}
 \fun{val Term.mkRel          : int -> constr}
-    {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.}
+    {$(\texttt{mkRel}\;n)$ represents deBruijn's index $n$.}
 
 \fun{val Term.mkVar : identifier -> constr} 
     {$(\texttt{mkVar}\;id)$
@@ -545,7 +545,7 @@ following constructor functions:
 
 \fun{val Term.mkProd : name ->constr ->constr -> constr}
     {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
-     The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     The free ocurrences of $x$ in $B$ are represented by deBruijn's
      indexes.}
 
 \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
@@ -553,14 +553,14 @@ following constructor functions:
      but the bound occurrences of $x$ in $B$ are denoted by 
      the identifier $(\texttt{mkVar}\;x)$. The function automatically 
      changes each occurrences of this identifier into the corresponding 
-     deBrujin's index.}
+     deBruijn's index.}
 
 \fun{val Term.mkArrow : constr -> constr -> constr}
     {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}
 
 \fun{val Term.mkLambda       : name -> constr -> constr -> constr}
     {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
-     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBruijn's
      indexes.}
 
 \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
@@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic}
 \item Restoring type coercions and synthesizing the implicit arguments
 (the one denoted by question marks in
 {\Coq} syntax: see Section~\ref{Coercions}).
-\item Transforming the named bound variables into deBrujin's indexes.
+\item Transforming the named bound variables into deBruijn's indexes.
 \item Classifying the global names into the different classes of
 constants (defined constants, constructors, inductive types, etc).
 \end{enumerate}
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

---
 doc/RecTutorial/coqartmacros.tex |  2 +-
 doc/refman/RefMan-tus.tex        | 18 +++++++++---------
 2 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'doc')

diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex
index 2a2c211963..72d7492690 100644
--- a/doc/RecTutorial/coqartmacros.tex
+++ b/doc/RecTutorial/coqartmacros.tex
@@ -149,7 +149,7 @@
 \newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}%
                         \end{bundle}}
 
-% the same in DeBruijn form
+% the same in de Bruijn form
 \newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}
                        \end{bundle}}
 
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index c55b3775cf..017de6d484 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -288,8 +288,8 @@ constructors:
 \item $(\texttt{VAR}\;id)$, a reference to a global identifier called  $id$;
 \item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$
       binder up in the term;
-\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$;
-\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of 
+\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$;
+\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of
       the vector $vt$;
 \item $(\texttt{DOP0}\;op)$, a unary operator $op$;
 \item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary
@@ -299,7 +299,7 @@ vector of terms $vt$.
 \end{itemize}
 
 In this meta-language, bound variables are represented using the
-so-called deBruijn's indexes. In this representation, an occurrence of
+so-called de Bruijn's indexes. In this representation, an occurrence of
 a bound variable is denoted by an integer, meaning the number of
 binders that must be traversed to reach its own
 binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
@@ -339,7 +339,7 @@ on the terms of the meta-language:
 \fun{val Generic.dependent : 'op term -> 'op term -> bool}
     {Returns true if the first term is a sub-term of the second.}
 %\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term}
-%    { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index
+%    { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index
 %     associated to $id$ to every occurrence of the term
 %    $(\texttt{VAR}\;id)$ in $t$.}
 \end{description}
@@ -482,7 +482,7 @@ following constructor functions:
 
 \begin{description}
 \fun{val Term.mkRel          : int -> constr}
-    {$(\texttt{mkRel}\;n)$ represents deBruijn's index $n$.}
+    {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.}
 
 \fun{val Term.mkVar : identifier -> constr} 
     {$(\texttt{mkVar}\;id)$
@@ -545,7 +545,7 @@ following constructor functions:
 
 \fun{val Term.mkProd : name ->constr ->constr -> constr}
     {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
-     The free ocurrences of $x$ in $B$ are represented by deBruijn's
+     The free ocurrences of $x$ in $B$ are represented by de Bruijn's
      indexes.}
 
 \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
@@ -553,14 +553,14 @@ following constructor functions:
      but the bound occurrences of $x$ in $B$ are denoted by 
      the identifier $(\texttt{mkVar}\;x)$. The function automatically 
      changes each occurrences of this identifier into the corresponding 
-     deBruijn's index.}
+     de Bruijn's index.}
 
 \fun{val Term.mkArrow : constr -> constr -> constr}
     {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}
 
 \fun{val Term.mkLambda       : name -> constr -> constr -> constr}
     {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
-     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBruijn's
+     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's
      indexes.}
 
 \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
@@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic}
 \item Restoring type coercions and synthesizing the implicit arguments
 (the one denoted by question marks in
 {\Coq} syntax: see Section~\ref{Coercions}).
-\item Transforming the named bound variables into deBruijn's indexes.
+\item Transforming the named bound variables into de Bruijn's indexes.
 \item Classifying the global names into the different classes of
 constants (defined constants, constructors, inductive types, etc).
 \end{enumerate}
-- 
cgit v1.2.3


From 4a84961049f4f00897ae72a13954edbcc9aaba5e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 3 May 2017 10:23:46 +0200
Subject: Fix outdated description in RefMan.

---
 doc/refman/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c37367de5b..4c333379bd 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -118,7 +118,7 @@ the current proof and declare the initial goal as an axiom.
 \subsection[\tt Proof {\term}.]{\tt Proof {\term}.\comindex{Proof}
 \label{BeginProof}}
 This command applies in proof editing mode. It is equivalent to {\tt
-  exact {\term}; Save.} That is, you have to give the full proof in
+  exact {\term}. Qed.} That is, you have to give the full proof in
 one gulp, as a proof term (see Section~\ref{exact}).
 
 \variant {\tt Proof.}
-- 
cgit v1.2.3


From 4cc655377e3c73fd3066cd8136d17605f167ef56 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 4 May 2017 10:28:56 +0200
Subject: Improve documentation of assert / pose proof / specialize.

This commits documents the as clause of specialize and that the
as clause of pose proof is optional.

It also mentions a feature of assert ( := ) that was available
since 8.5 and was mentionned by @herbelin in:
https://github.com/coq/coq/pull/248#issuecomment-297970503
---
 doc/refman/RefMan-tac.tex | 28 ++++++++++++++++++----------
 1 file changed, 18 insertions(+), 10 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0edc66f839..87b9e4914f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1275,15 +1275,18 @@ in the list of subgoals remaining to prove.
 
 \item{\tt assert ( {\ident} := {\term} )}
 
-  This behaves as {\tt assert ({\ident} :\ {\type});[exact
-      {\term}|idtac]} where {\type} is the type of {\term}. This is
-  deprecated in favor of {\tt pose proof}.
+  This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}}
+  where {\type} is the type of {\term}. This is deprecated in favor of
+  {\tt pose proof}.
+
+  If the head of {\term} is {\ident}, the tactic behaves as
+  {\tt specialize \term}.
 
   \ErrMsg \errindex{Variable {\ident} is already declared}
 
-\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}}
+\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}}
 
-  This tactic behaves like \texttt{assert T as {\intropattern} by
+  This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by
   exact {\term}} where \texttt{T} is the type of {\term}.
 
   In particular, \texttt{pose proof {\term} as {\ident}} behaves as
@@ -1326,8 +1329,8 @@ in the list of subgoals remaining to prove.
   following subgoals: {\tt U -> T} and \texttt{U}.  The subgoal {\tt U
     -> T} comes first in the list of remaining subgoal to prove.
 
-\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\
-      {\tt specialize {\ident} with \bindinglist}
+\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\
+      {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}}
 
       The tactic {\tt specialize} works on local hypothesis \ident.
       The premises of this hypothesis (either universal
@@ -1338,14 +1341,19 @@ in the list of subgoals remaining to prove.
       second form, all instantiation elements must be given, whereas
       in the first form the application to \term$_1$ {\ldots}
       \term$_n$ can be partial. The first form is equivalent to
-      {\tt assert (\ident' := {\ident} {\term$_1$} \dots\ \term$_n$);
-           clear \ident; rename \ident' into \ident}.
+      {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}.
+
+      With the {\tt as} clause, the local hypothesis {\ident} is left
+      unchanged and instead, the modified hypothesis is introduced as
+      specified by the {\intropattern}.
 
       The name {\ident} can also refer to a global lemma or
       hypothesis. In this case, for compatibility reasons, the
       behavior of {\tt specialize} is close to that of {\tt
         generalize}: the instantiated statement becomes an additional
-      premise of the goal.
+      premise of the goal. The {\tt as} clause is especially useful
+      in this case to immediately introduce the instantiated statement
+      as a local hypothesis.
 
   \begin{ErrMsgs}
   \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis}
-- 
cgit v1.2.3


From 06f3ce00971283d2718e272ec9f123430d75ffa6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 11 May 2017 15:16:21 +0200
Subject: Documenting Printing Compact Contexts + CHANGES

---
 doc/refman/RefMan-oth.tex | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 56ce753cd6..0f6978b255 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -960,6 +960,22 @@ time of writing this documentation, the default value is 50).
 \subsection[\tt Test Printing Depth.]{\tt Test Printing Depth.\optindex{Printing Depth}}
 This command displays the current nesting depth used for display.
 
+\subsection[\tt Unset Printing Compact Contexts.]{\tt Unset Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command resets the displaying of goals contexts to non compact
+mode (default at the time of writing this documentation). Non compact
+means that consecutive variables of different types are printed on
+different lines.
+
+\subsection[\tt Set Printing Compact Contexts.]{\tt Set Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command sets the displaying of goals contexts to compact mode.
+The printer tries to reduce the vertical size of goals contexts by
+putting several variables (even if of different types) on the same
+line provided it does not exceed the printing width (See {\tt Set
+  Printing Width} above).
+
+\subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}}
+This command displays the current state of compaction of goal d'isolat.
+
 \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
 This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
 line when {\tt -emacs} is passed.
-- 
cgit v1.2.3


From 6c9fb0b16fa5674a3135a49adff201d6e4415cd1 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 10 May 2017 20:48:37 -0400
Subject: Add documentation for Set Ltac Batch Debug

---
 doc/refman/RefMan-ltac.tex | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c2f52e23bc..0346c4a555 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1242,7 +1242,7 @@ This will automatically print the same trace as {\tt Info \num} at each tactic c
 
 The current value for the {\tt Info Level} option can be checked using the {\tt Test Info Level} command.
 
-\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}}
+\subsection[Interactive debugger]{Interactive debugger\optindex{Ltac Debug}\optindex{Ltac Batch Debug}}
 
 The {\ltac} interpreter comes with a step-by-step debugger. The
 debugger can be activated using the command
@@ -1273,6 +1273,17 @@ r $n$: & advance $n$ steps further\\
 r {\qstring}: & advance up to the next call to ``{\tt idtac} {\qstring}''\\
 \end{tabular}
 
+A non-interactive mode for the debugger is available via the command
+
+\begin{quote}
+{\tt Set Ltac Batch Debug.}
+\end{quote}
+
+This option has the effect of presenting a newline at every prompt,
+when the debugger is on.  The debug log thus created, which does not
+require user input to generate when this option is set, can then be
+run through external tools such as \texttt{diff}.
+
 \subsection[Profiling {\ltac} tactics]{Profiling {\ltac} tactics\optindex{Ltac Profiling}\comindex{Show Ltac Profile}\comindex{Reset Ltac Profile}}
 
 It is possible to measure the time spent in invocations of primitive tactics as well as tactics defined in {\ltac} and their inner invocations. The primary use is the development of complex tactics, which can sometimes be so slow as to impede interactive usage. The reasons for the performence degradation can be intricate, like a slowly performing {\ltac} match or a sub-tactic whose performance only degrades in certain situations. The profiler generates a call tree and indicates the time spent in a tactic depending its calling context. Thus it allows to locate the part of a tactic definition that contains the performance bug.
-- 
cgit v1.2.3


From 80fc13e3115058230586246e72d69e3eac467f73 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 24 Mar 2017 21:13:38 +0100
Subject: Documenting relaxing of constraints on injection.

We seized this opportunity to do a little refreshing of the section
describing injection.
---
 doc/refman/RefMan-tac.tex | 39 ++++++++++++++++-----------------------
 1 file changed, 16 insertions(+), 23 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 87b9e4914f..fc3fdd0025 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2187,32 +2187,24 @@ the given bindings to instantiate parameters or hypotheses of {\term}.
 \label{injection}
 \tacindex{injection}
 
-The {\tt injection} tactic is based on the fact that constructors of
-inductive sets are injections. That means that if $c$ is a constructor
-of an inductive set, and if $(c~\vec{t_1})$ and $(c~\vec{t_2})$ are two
-terms that are equal then $~\vec{t_1}$ and $~\vec{t_2}$ are equal
-too.
+The {\tt injection} tactic exploits the property that constructors of
+inductive types are injective, i.e. that if $c$ is a constructor
+of an inductive type and $c~\vec{t_1}$ and $c~\vec{t_2}$ are equal
+then $\vec{t_1}$ and $\vec{t_2}$ are equal too.
 
 If {\term} is a proof of a statement of conclusion
  {\tt {\term$_1$} = {\term$_2$}},
-then {\tt injection} applies injectivity as deep as possible to
-derive the equality of all the subterms of {\term$_1$} and {\term$_2$}
-placed in the same positions. For example, from {\tt (S
-  (S n))=(S (S (S m)))} we may derive {\tt n=(S m)}.  To use this
-tactic {\term$_1$} and {\term$_2$} should be elements of an inductive
-set and they should be neither explicitly equal, nor structurally
-different. We mean by this that, if {\tt n$_1$} and {\tt n$_2$} are
-their respective normal forms, then:
-\begin{itemize}
-\item {\tt n$_1$} and {\tt n$_2$} should not be syntactically equal,
-\item there must not exist any pair of subterms {\tt u} and {\tt w},
-  {\tt u} subterm of {\tt n$_1$} and {\tt w} subterm of {\tt n$_2$} ,
-  placed in the same positions and having different constructors as
-  head symbols.
-\end{itemize}
-If these conditions are satisfied, then, the tactic derives the
-equality of all the subterms of {\term$_1$} and {\term$_2$} placed in
-the same positions and puts them as antecedents of the current goal.
+then {\tt injection} applies the injectivity of constructors as deep as possible to
+derive the equality of all the subterms of {\term$_1$} and {\term$_2$} at positions
+where {\term$_1$} and {\term$_2$} start to differ.
+For example, from {\tt (S p, S n) = (q, S (S m)} we may derive {\tt S
+  p = q} and {\tt n = S m}. For this tactic to work, {\term$_1$} and
+{\term$_2$} should be typed with an inductive
+type and they should be neither convertible, nor having a different
+head constructor. If these conditions are satisfied, the tactic
+derives the equality of all the subterms of {\term$_1$} and
+{\term$_2$} at positions where they differ and adds them as
+antecedents to the conclusion of the current goal.
 
 \Example Consider the following goal:
 
@@ -2251,6 +2243,7 @@ context using \texttt{intros until \ident}.
 \item \errindex{Not a projectable equality but a discriminable one}
 \item \errindex{Nothing to do, it is an equality between convertible terms}
 \item \errindex{Not a primitive equality}
+\item \errindex{Nothing to inject}
 \end{ErrMsgs}
 
 \begin{Variants}
-- 
cgit v1.2.3


From 3c0d8d08bda81b9fbd7210e4e352a08bbe8219e8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 20:55:32 +0200
Subject: [vernac] Remove `Save.` command.

It has been deprecated for a while in favor of `Qed`.
---
 doc/refman/RefMan-pro.tex | 5 -----
 doc/refman/RefMan-tus.tex | 2 +-
 doc/tutorial/Tutorial.tex | 8 +++-----
 3 files changed, 4 insertions(+), 11 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8ba28b32f1..7e2b9db24d 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -90,11 +90,6 @@ memory overflow.
 
   Defines the proved term as a transparent constant.
 
-\item {\tt Save.}
-\comindex{Save}
-
-  This is a deprecated equivalent to {\tt Qed}.
-
 \item {\tt Save {\ident}.}
   
   Forces the name of the original goal to be {\ident}.  This command
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 017de6d484..7e5bb81a90 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -707,7 +707,7 @@ Once all the existential variables have been defined the derivation is
 completed, and a construction can be generated from the proof tree,
 replacing each of the existential variables by its definition.  This
 is exactly what happens when one of the commands
-\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
+\texttt{Qed} or \texttt{Defined} is invoked
 (see Section~\ref{Qed}). The saved theorem becomes a defined constant,
 whose body is the proof object generated.
 
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 0d537256bb..30b6304c16 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -385,13 +385,11 @@ apply H; [ assumption | apply H0; assumption ].
 
 Let us now save lemma \verb:distr_impl::
 \begin{coq_example}
-Save.
+Qed.
 \end{coq_example}
 
-Here \verb:Save: needs no argument, since we gave the name \verb:distr_impl: 
-in advance;
-it is however possible to override the given name by giving a different 
-argument to command \verb:Save:.
+Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl: 
+in advance.
 
 Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
 and \verb:assumption: may be found completely automatically by an automatic
-- 
cgit v1.2.3


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 doc/refman/RefMan-pro.tex | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 7e2b9db24d..0760d716e3 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -96,14 +96,6 @@ memory overflow.
   (and the following ones) can only be used if the original goal has
   been opened using the {\tt Goal} command.
 
-\item {\tt Save Theorem {\ident}.} \\
- {\tt Save Lemma {\ident}.} \\
- {\tt Save Remark {\ident}.}\\
- {\tt Save Fact {\ident}.}
- {\tt Save Corollary {\ident}.}
- {\tt Save Proposition {\ident}.}
-
-  Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
 \subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
-- 
cgit v1.2.3