Merge PR #7162: Sphinx doc chapter 7

8 files changed, 612 insertions, 598 deletions

diff --git a/Makefile.doc b/Makefile.doc
index fc791ce1c0..a8b5376a61 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -59,7 +59,6 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex
 REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-gal.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
-  RefMan-pro.v.tex \
   Universes.v.tex)
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
deleted file mode 100644
index bd74a40d7c..0000000000
--- a/doc/refman/RefMan-pro.tex
+++ /dev/null
@@ -1,581 +0,0 @@
-\chapter[Proof handling]{Proof handling\index{Proof editing}
-\label{Proof-handling}}
-%HEVEA\cutname{proof-handling.html}
-
-In \Coq's proof editing mode all top-level commands documented in 
-Chapter~\ref{Vernacular-commands} remain available
-and the user has access to specialized commands dealing with proof
-development pragmas documented in this section. He can also use some
-other specialized commands called {\em tactics}.  They are the very
-tools allowing the user to deal with logical reasoning. They are
-documented in Chapter~\ref{Tactics}.\\ 
-When switching in editing proof mode, the prompt
-\index{Prompt} 
-{\tt Coq <} is changed into {\tt {\ident} <} where {\ident} is the
-declared name of the theorem currently edited.
-
-At each stage of a proof development, one has a list of goals to
-prove. Initially, the list consists only in the theorem itself. After
-having applied some tactics, the list of goals contains the subgoals
-generated by the tactics.
-
-To each subgoal is associated  a number of
-hypotheses called the {\em \index*{local context}} of the goal.
-Initially, the local context contains the local variables and
-hypotheses of the current section (see Section~\ref{Variable}) and the
-local variables and hypotheses of the theorem statement.  It is
-enriched by the use of certain tactics (see e.g. {\tt intro} in
-Section~\ref{intro}).
-
-When a proof is completed, the message {\tt Proof completed} is
-displayed. One can then register this proof as a defined constant in the
-environment. Because there exists a correspondence between proofs and
-terms of $\lambda$-calculus, known as the {\em Curry-Howard
-isomorphism} \cite{How80,Bar91,Gir89,Hue89}, \Coq~ stores proofs as
-terms of {\sc Cic}. Those terms are called {\em proof
-  terms}\index{Proof term}.
-
-\ErrMsg When one attempts to use a proof editing command out of the
-proof editing mode, \Coq~ raises the error message : \errindex{No focused
-  proof}.
-
-\section{Switching on/off the proof editing mode}
-
-The proof editing mode is entered by asserting a statement, which
-typically is the assertion of a theorem:
-
-\begin{quote}
-{\tt Theorem {\ident} \zeroone{\binders} : {\form}.\comindex{Theorem}
-\label{Theorem}}
-\end{quote}
-
-The list of assertion commands is given in
-Section~\ref{Assertions}. The command {\tt Goal} can also be used.
-
-\subsection[Goal {\form}.]{\tt Goal {\form}.\comindex{Goal}\label{Goal}}
-
-This is intended for quick assertion of statements, without knowing in
-advance which name to give to the assertion, typically for quick
-testing of the provability of a statement. If the proof of the
-statement is eventually completed and validated, the statement is then
-bound to the name {\tt Unnamed\_thm} (or a variant of this name not
-already used for another statement).
-
-\subsection[\tt Qed.]{\tt Qed.\comindex{Qed}\label{Qed}}
-This command is available in interactive editing proof mode when the
-proof is completed.  Then {\tt Qed} extracts a proof term from the
-proof script, switches back to {\Coq} top-level and attaches the
-extracted proof term to the declared name of the original goal. This
-name is added to the environment as an {\tt Opaque} constant.
-
-\begin{ErrMsgs}
-\item \errindex{Attempt to save an incomplete proof}
-%\item \ident\ \errindex{already exists}\\ 
-%  The implicit name is already defined. You have then to provide
-%  explicitly a new name (see variant 3 below).
-\item Sometimes an error occurs when building the proof term,
-because tactics do not enforce completely the term construction
-constraints.
-
-The user should also be aware of the fact that since the proof term is
-completely rechecked at this point, one may have to wait a while when
-the proof is large. In some exceptional cases one may even incur a
-memory overflow.
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Defined.}
-\comindex{Defined} 
-\label{Defined} 
-
-  Defines the proved term as a transparent constant.
-
-\item {\tt Save {\ident}.}
-  
-  Forces the name of the original goal to be {\ident}.  This command
-  (and the following ones) can only be used if the original goal has
-  been opened using the {\tt Goal} command.
-
-\end{Variants}
-
-\subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
-This command is available in interactive editing proof mode to give up
-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}. Qed.} That is, you have to give the full proof in
-one gulp, as a proof term (see Section~\ref{exact}).
-
-\variant {\tt Proof.}
-  
-  Is a noop which is useful to delimit the sequence of tactic commands
-  which start a proof, after a {\tt Theorem} command.  It is a good
-  practice to use {\tt Proof.} as an opening parenthesis, closed in
-  the script with a closing {\tt Qed.}
-
-\SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
-
-\subsection[{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}]
-{{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}
-\comindex{Proof using} \label{ProofUsing}}
-
-This command applies in proof editing mode. 
-It declares the set of section variables (see~\ref{Variable}) 
-used by the proof. At {\tt Qed} time, the system will assert that 
-the set of section variables actually used in the proof is a subset of
-the declared one.
-
-The set of declared variables is closed under type dependency.
-For example if {\tt T} is variable and {\tt a} is a variable of
-type {\tt T}, the commands {\tt Proof using a} and
-{\tt Proof using T a} are actually equivalent.
-
-\variant {\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$} {\tt with} {\tac}{\tt .} 
-in Section~\ref{ProofWith}.
-
-\variant {\tt Proof using All.} 
-
-  Use all section variables.
-
-\variant {\tt Proof using Type.} 
-\variant {\tt Proof using.} 
-  
-  Use only section variables occurring in the statement.
-
-\variant {\tt Proof using Type*.} 
-  
-  The {\tt *} operator computes the forward transitive closure.
-  E.g. if the variable {\tt H} has type {\tt p < 5} then {\tt H} is
-  in {\tt p*} since {\tt p} occurs in the type of {\tt H}.
-  {\tt Type* } is the forward transitive closure of the entire set of
-  section variables occurring in the statement.
-
-\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$  ).}
-  
-  Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}.
-
-\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .}
-
-\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .}
-
-\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).}
-
-\variant {\tt Proof using \nterm{collection} * .}
-
-  Use section variables being, respectively, in the set union, set difference,
-  set complement, set forward transitive closure.
-  See Section~\ref{Collection} to know how to form a named
-  collection.
-  The {\tt *} operator binds stronger than {\tt +} and {\tt -}.
-
-\subsubsection{{\tt Proof using} options}
-\optindex{Default Proof Using}
-\optindex{Suggest Proof Using}
-% \optindex{Proof Using Clear Unused}
-
-The following options modify the behavior of {\tt Proof using}.
-
-\variant {\tt Set Default Proof Using "expression".} 
-
-  Use {\tt expression} as the default {\tt Proof using} value.
-  E.g. {\tt Set Default Proof Using "a b".} will complete all {\tt Proof }
-  commands not followed by a {\tt using} part with {\tt using a b}.
-
-\variant {\tt Set Suggest Proof Using.}
-
-  When {\tt Qed} is performed, suggest a {\tt using} annotation if
-  the user did not provide one.
-
-% \variant{\tt Unset Proof Using Clear Unused.}
-% 
-%   When {\tt Proof using a} all section variables but for {\tt a} and
-%   the variables used in the type of {\tt a} are cleared.
-%   This option can be used to turn off this behavior.
-% 
-\subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
-\comindex{Collection}\label{Collection}
-
-The command {\tt Collection} can be used to name a set of section hypotheses,
-with the purpose of making {\tt Proof using} annotations more compact.
-
-\variant {\tt Collection Some := x y z.}
-
-  Define the collection named "Some" containing {\tt x y} and {\tt z} 
-
-\variant {\tt Collection Fewer := Some - x.} 
-  
-  Define the collection named "Fewer" containing only {\tt x y} 
-
-\variant {\tt Collection Many := Fewer + Some.} 
-\variant {\tt Collection Many := Fewer - Some.} 
-  
-  Define the collection named "Many" containing the set union or set difference
-  of "Fewer" and "Some".
-
-\variant {\tt Collection Many := Fewer - (x y).}
-
-  Define the collection named "Many" containing the set difference
-  of "Fewer" and the unnamed collection {\tt x y}.
-
-\subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
-
-This command cancels the current proof development, switching back to
-the previous proof development, or to the \Coq\ toplevel if no other
-proof was edited.
-
-\begin{ErrMsgs}
-\item \errindex{No focused proof (No proof-editing in progress)}
-\end{ErrMsgs}
-
-\begin{Variants}
-
-\item {\tt Abort {\ident}.}
-
-  Aborts the editing of the proof named {\ident}.
-
-\item {\tt Abort All.}
-
-  Aborts all current goals, switching back to the \Coq\ toplevel.
-
-\end{Variants}
-
-%%%%
-\subsection[\tt Existential {\num} := {\term}.]{\tt Existential  {\num} := {\term}.\comindex{Existential}
-\label{Existential}}
-
-This command instantiates an existential variable. {\tt \num}
-is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials} (described in Section~\ref{Show}).
-
-This command is intended to be used to instantiate existential
-variables when the proof is completed but some uninstantiated
-existential variables remain. To instantiate existential variables
-during proof edition, you should use the tactic {\tt instantiate}.
-
-\SeeAlso {\tt instantiate (\num:= \term).} in Section~\ref{instantiate}.
-\SeeAlso {\tt Grab Existential Variables.} below.
-
-\subsection[\tt Grab Existential Variables.]{\tt Grab Existential Variables.\comindex{Grab Existential Variables}
-\label{GrabEvars}}
-
-This command can be run when a proof has no more goal to be solved but has remaining
-uninstantiated existential variables. It takes every uninstantiated existential variable
-and turns it into a goal.
-
-%%%%%%%%
-\section{Navigation in the proof tree}
-%%%%%%%%
-
-\subsection[\tt Undo.]{\tt Undo.\comindex{Undo}}
-
-This command cancels the effect of the last command.  Thus, it
-backtracks one step.
-
-\begin{Variants}
-
-\item {\tt Undo {\num}.}
-
-  Repeats {\tt Undo} {\num} times.
-
-\end{Variants}
-
-\subsection[\tt Restart.]{\tt Restart.\comindex{Restart}}
-This command restores the proof editing process to the original goal.
-
-\begin{ErrMsgs}
-\item \errindex{No focused proof to restart}
-\end{ErrMsgs}
-
-\subsection[\tt Focus.]{\tt Focus.\comindex{Focus}}
-This focuses the attention on the first subgoal to prove and the printing
-of the other subgoals is suspended until the focused subgoal is
-solved or unfocused. This is useful when there are many current
-subgoals which clutter your screen.
-
-\begin{Variant}
-\item {\tt Focus {\num}.}\\ 
-This focuses the attention on the $\num^{th}$ subgoal to prove.
-\end{Variant}
-
-\emph{This command is deprecated since 8.8: prefer the use of bullets or
-  focusing brackets instead, including {\tt {\num}: \{}}.
-
-\subsection[\tt Unfocus.]{\tt Unfocus.\comindex{Unfocus}}
-This command restores to focus the goal that were suspended by the
-last {\tt Focus} command.
-
-\emph{This command is deprecated since 8.8.}
-
-\subsection[\tt Unfocused.]{\tt Unfocused.\comindex{Unfocused}}
-Succeeds in the proof if fully unfocused, fails if there are some
-goals out of focus.
-
-\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
-The command {\tt \{} (without a terminating period) focuses on the
-first goal, much like {\tt Focus.} does, however, the subproof can
-only be unfocused when it has been fully solved (\emph{i.e.} when
-there is no focused goal left). Unfocusing is then handled by {\tt \}}
-(again, without a terminating period). See also example in next section.
-
-Note that when a focused goal is proved a message is displayed
-together with a suggestion about the right bullet or {\tt \}} to
-unfocus it or focus the next one.
-
-\begin{Variants}
-
-\item {\tt {\num}: \{}\\
-This focuses on the $\num^{th}$ subgoal to prove.
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{This proof is focused, but cannot be unfocused
-    this way} You are trying to use {\tt \}} but the current subproof
-  has not been fully solved.
-\item \errindex{No such goal}
-\item \errindex{Brackets only support the single numbered goal selector}
-\item see also error message about bullets below.
-\end{ErrMsgs}
-
-\subsection[Bullets]{Bullets\comindex{+ (command)}
-  \comindex{- (command)}\comindex{* (command)}\index{Bullets}}\label{bullets}
-Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with
-bullets. The use of a bullet $b$ for the first time focuses on the
-first goal $g$, the same bullet cannot be used again until the proof
-of $g$ is completed, then it is mandatory to focus the next goal with $b$. The
-consequence is that $g$ and all goals present when $g$ was focused are
-focused with the same bullet $b$. See the example below.
-
-Different bullets can be used to nest levels. The scope of bullet does
-not go beyond enclosing {\tt \{} and {\tt \}}, so bullets can be
-reused as further nesting levels provided they are delimited by these.
-Available bullets are {\tt -}, {\tt +}, {\tt *}, {\tt --}, {\tt ++}, {\tt **},
-{\tt ---}, {\tt +++}, {\tt ***}, ... (without a
-terminating period).
-
-Note again that when a focused goal is proved a message is displayed
-together with a suggestion about the right bullet or {\tt \}} to
-unfocus it or focus the next one.
-
-Remark: In {\ProofGeneral} (Emacs interface to {\Coq}), you must use
-bullets with the priority ordering shown above to have a correct
-indentation. For example {\tt -} must be the outer bullet and {\tt **}
-the inner one in the example below.
-
-The following example script illustrates all these features:
-\begin{coq_example*}
-Goal (((True/\True)/\True)/\True)/\True.
-Proof.
-  split.
-  - split.
-    + split.
-      ** { split.
-          - trivial.
-          - trivial.
-        }
-      ** trivial.
-    + trivial.
-  - assert True.
-    { trivial. }
-    assumption.
-\end{coq_example*}
-
-
-\begin{ErrMsgs}
-\item \errindex{Wrong bullet {\abullet}1 : Current bullet
-    {\abullet}2 is not finished.}
-
-  Before using bullet {\abullet}1 again, you should first finish
-  proving the current focused goal. Note that {\abullet}1 and
-  {\abullet}2 may be the same.
-
-\item \errindex{Wrong bullet {\abullet}1 : Bullet {\abullet}2
-    is mandatory here.} You must put {\abullet}2 to focus next goal.
-  No other bullet is allowed here.
-
-
-\item \errindex{No such goal. Focus next goal with bullet
-    {\abullet}.}
-
-  You tried to applied a tactic but no goal where under focus. Using
-  {\abullet} is mandatory here.
-
-\item \errindex{No such goal. Try unfocusing with {"{\tt \}}"}.} You
-  just finished a goal focused by {\tt \{}, you must unfocus it with "{\tt \}}".
-
-\end{ErrMsgs}
-
-\subsection[\tt Set Bullet Behavior.]{\tt Set Bullet Behavior.\optindex{Bullet Behavior}}
-
-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}
-
-\subsection[\tt Show.]{\tt Show.\comindex{Show}\label{Show}}
-This command displays the current goals.
-
-\begin{Variants}
-\item {\tt Show {\num}.}\\ 
-  Displays only the {\num}-th subgoal.\\ 
-\begin{ErrMsgs}
-\item \errindex{No such goal}
-\item \errindex{No focused proof}
-\end{ErrMsgs}
-
-\item {\tt Show {\ident}.}\\
-  Displays the named goal {\ident}.
-  This is useful in particular to display a shelved goal but only works
-  if the corresponding existential variable has been named by the user
-  (see~\ref{ExistentialVariables}) as in the following example.
-
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{coq_example*}
-Goal exists n, n = 0.
-  eexists ?[n].
-\end{coq_example*}
-\begin{coq_example}
-  Show n.
-\end{coq_example}
-
-\item {\tt Show Script.}\comindex{Show Script}\\
-  Displays the whole list of tactics applied from the beginning
-  of the current proof. 
-  This tactics script may contain some holes (subgoals not yet proved).
-  They are printed under the form \verb!<Your Tactic Text here>!.
-
-\item {\tt Show Proof.}\comindex{Show Proof}\\
-It displays the proof term generated by the 
-tactics that have been applied. 
-If the proof is not completed, this term contain holes,
-which correspond to the sub-terms which are still to be 
-constructed. These holes appear as a question mark indexed 
-by an integer, and applied to the list of variables in 
-the context, since it may depend on them. 
-The types obtained by abstracting away the context from the
-type of each hole-placer are also printed.
-
-\item {\tt Show Conjectures.}\comindex{Show Conjectures}\\
-It prints the list of the names of all the theorems that 
-are currently being proved.
-As it is possible to start proving a previous lemma during
-the proof of a theorem, this list may contain several 
-names. 
-
-\item{\tt Show Intro.}\comindex{Show Intro}\\
-If the current goal begins by at least one product, this command
-prints the name of the first product, as it would be generated by 
-an anonymous {\tt intro}. The aim of this command is to ease the
-writing of more robust scripts. For example, with an appropriate 
-{\ProofGeneral} macro, it is possible to transform any anonymous {\tt
-  intro} into a qualified one such as {\tt intro y13}.
-In the case of a non-product goal, it prints nothing. 
-
-\item{\tt Show Intros.}\comindex{Show Intros}\\
-This command is similar to the previous one, it simulates the naming 
-process of an {\tt intros}.
-
-\item{\tt Show Existentials.\label{ShowExistentials}}\comindex{Show Existentials}
-\\ It displays
-the set of all uninstantiated existential variables in the current proof tree, 
-along with the type and the context of each variable.
-
-\item{\tt Show Match {\ident}.\label{ShowMatch}}\comindex{Show Match}\\
-This variant displays a template of the Gallina {\tt match} construct 
-with a branch for each constructor of the type {\ident}.
-
-Example:
-
-\begin{coq_example}
-Show Match nat.  
-\end{coq_example}
-\begin{ErrMsgs}
-\item \errindex{Unknown inductive type}
-\end{ErrMsgs}
-
-\item{\tt Show Universes.\label{ShowUniverses}}\comindex{Show Universes}
-\\ It displays the set of all universe constraints and its
-normalized form at the current stage of the proof, useful for
-debugging universe inconsistencies.
-
-\end{Variants}
-
-
-\subsection[\tt Guarded.]{\tt Guarded.\comindex{Guarded}\label{Guarded}}
-
-Some tactics (e.g. refine \ref{refine}) allow to build proofs using
-fixpoint or co-fixpoint constructions. Due to the incremental nature
-of interactive proof construction, the check of the termination (or
-guardedness) of the recursive calls in the fixpoint or cofixpoint
-constructions is postponed to the time of the completion of the proof.
-
-The command \verb!Guarded! allows checking if the guard condition for
-fixpoint and cofixpoint is violated at some time of the construction
-of the proof without having to wait the completion of the proof."
-
-
-\section{Controlling the effect of proof editing commands}
-
-\subsection[\tt Set Hyps Limit {\num}.]{\tt Set Hyps Limit {\num}.\optindex{Hyps Limit}}
-This command sets the maximum number of hypotheses displayed in
-goals after the application of a tactic. 
-All the hypotheses remains usable in the proof development.
-
-
-\subsection[\tt Unset Hyps Limit.]{\tt Unset Hyps Limit.\optindex{Hyps Limit}}
-This command goes back to the default mode which is to print all
-available hypotheses.
-
-
-\subsection[\tt Set Automatic Introduction.]{\tt Set Automatic Introduction.\optindex{Automatic Introduction}\label{Set Automatic Introduction}}
-
-The option {\tt Automatic Introduction} controls the way binders are
-handled in assertion commands such as {\tt Theorem {\ident}
-  \zeroone{\binders} : {\form}}. When the option is set, which is the
-default, {\binders} are automatically put in the local context of the
-goal to prove.
-
-The option can be unset by issuing {\tt Unset Automatic Introduction}.
-When the option is unset, {\binders} are discharged on the statement
-to be proved and a tactic such as {\tt intro} (see
-Section~\ref{intro}) has to be used to move the assumptions to the
-local context.
-
-\section{Controlling memory usage\comindex{Optimize Proof}\comindex{Optimize Heap}}
-
-When experiencing high memory usage the following commands can be
-used to force Coq to optimize some of its internal data structures.
-
-\subsection[\tt Optimize Proof.]{\tt Optimize Proof.}
-
-This command forces Coq to shrink the data structure used to represent
-the ongoing proof.
-
-\subsection[\tt Optimize Heap.]{\tt Optimize Heap.\label{vernac-optimizeheap}}
-
-This command forces the OCaml runtime to perform a heap compaction.
-This is in general an expensive operation.  See: \\
-\ \url{http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact} \\
-There is also an analogous tactic {\tt optimize\_heap} (see~\ref{tactic-optimizeheap}).
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End: 
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index e511160075..8909c0fefd 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -99,7 +99,6 @@ Options A and B of the licence are {\em not} elected.}
 
 \part{The proof engine}
 \include{RefMan-oth.v}% Vernacular commands
-\include{RefMan-pro.v}% Proof handling
 \include{RefMan-ltac.v}% Writing tactics
 
 \lstset{language=SSR}
diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst
index db03693ff9..e2824d7ca8 100644
--- a/doc/sphinx/index.rst
+++ b/doc/sphinx/index.rst
@@ -24,6 +24,7 @@ Table of contents
 .. toctree::
    :caption: The proof engine
 
+   proof-engine/proof-handling
    proof-engine/tactics
    proof-engine/detailed-tactic-examples
    proof-engine/ssreflect-proof-language
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
new file mode 100644
index 0000000000..52cde52c69
--- /dev/null
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -0,0 +1,592 @@
+.. include:: ../replaces.rst
+.. _proofhandling:
+
+-------------------
+ Proof handling
+-------------------
+
+In |Coq|’s proof editing mode all top-level commands documented in
+Chapter :ref:`vernacularcommands` remain available and the user has access to specialized
+commands dealing with proof development pragmas documented in this
+section. He can also use some other specialized commands called
+*tactics*. They are the very tools allowing the user to deal with
+logical reasoning. They are documented in Chapter :ref:`tactics`.
+When switching in editing proof mode, the prompt ``Coq <`` is changed into
+``ident <`` where ``ident`` is the declared name of the theorem currently
+edited.
+
+At each stage of a proof development, one has a list of goals to
+prove. Initially, the list consists only in the theorem itself. After
+having applied some tactics, the list of goals contains the subgoals
+generated by the tactics.
+
+To each subgoal is associated a number of hypotheses called the *local
+context* of the goal. Initially, the local context contains the local
+variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`)
+and the local variables and hypotheses of the theorem statement. It is
+enriched by the use of certain tactics (see e.g. ``intro`` in Section
+:ref:`managingthelocalcontext`).
+
+When a proof is completed, the message ``Proof completed`` is displayed.
+One can then register this proof as a defined constant in the
+environment. Because there exists a correspondence between proofs and
+terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_,
+[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq|
+stores proofs as terms of |Cic|. Those terms
+are called *proof terms*.
+
+
+.. exn:: No focused proof
+
+Coq raises this error message when one attempts to use a proof editing command
+out of the proof editing mode.
+
+Switching on/off the proof editing mode
+-------------------------------------------
+
+The proof editing mode is entered by asserting a statement, which
+typically is the assertion of a theorem:
+
+.. cmd:: Theorem @ident [@binders] : @form.
+
+The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The
+command ``Goal`` can also be used.
+
+.. cmd:: Goal @form.
+
+This is intended for quick assertion of statements, without knowing in
+advance which name to give to the assertion, typically for quick
+testing of the provability of a statement. If the proof of the
+statement is eventually completed and validated, the statement is then
+bound to the name ``Unnamed_thm`` (or a variant of this name not already
+used for another statement).
+
+.. cmd:: Qed.
+
+This command is available in interactive editing proof mode when the
+proof is completed. Then ``Qed`` extracts a proof term from the proof
+script, switches back to Coq top-level and attaches the extracted
+proof term to the declared name of the original goal. This name is
+added to the environment as an ``Opaque`` constant.
+
+
+.. exn:: Attempt to save an incomplete proof
+
+.. note::
+
+   Sometimes an error occurs when building the proof term, because
+   tactics do not enforce completely the term construction
+   constraints.
+
+The user should also be aware of the fact that since the
+proof term is completely rechecked at this point, one may have to wait
+a while when the proof is large. In some exceptional cases one may
+even incur a memory overflow.
+
+.. cmdv:: Defined.
+
+Defines the proved term as a transparent constant.
+
+.. cmdv:: Save @ident.
+
+Forces the name of the original goal to be :n:`@ident`. This
+command (and the following ones) can only be used if the original goal
+has been opened using the ``Goal`` command.
+
+
+.. cmd:: Admitted.
+
+This command is available in interactive editing proof mode to give up
+the current proof and declare the initial goal as an axiom.
+
+
+.. cmd:: Proof @term.
+
+This command applies in proof editing mode. It is equivalent to
+
+.. cmd:: exact @term. Qed.
+
+That is, you have to give the full proof in one gulp, as a
+proof term (see Section :ref:`applyingtheorems`).
+
+
+.. cmdv:: Proof.
+
+Is a noop which is useful to delimit the sequence of tactic commands
+which start a proof, after a ``Theorem`` command. It is a good practice to
+use ``Proof``. as an opening parenthesis, closed in the script with a
+closing ``Qed``.
+
+
+See also: ``Proof with tactic.`` in Section
+:ref:`setimpautotactics`.
+
+
+.. cmd:: Proof using @ident1 ... @identn.
+
+This command applies in proof editing mode. It declares the set of
+section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the
+system will assert that the set of section variables actually used in
+the proof is a subset of the declared one.
+
+The set of declared variables is closed under type dependency. For
+example if ``T`` is variable and a is a variable of type ``T``, the commands
+``Proof using a`` and ``Proof using T a``` are actually equivalent.
+
+
+.. cmdv:: Proof using @ident1 ... @identn with @tactic.
+
+in Section :ref:`setimpautotactics`.
+
+.. cmdv:: Proof using All.
+
+Use all section variables.
+
+
+.. cmdv:: Proof using Type.
+
+.. cmdv:: Proof using.
+
+Use only section variables occurring in the statement.
+
+
+.. cmdv:: Proof using Type*.
+
+The ``*`` operator computes the forward transitive closure. E.g. if the
+variable ``H`` has type ``p < 5`` then ``H`` is in ``p*`` since ``p`` occurs in the type
+of ``H``. ``Type*`` is the forward transitive closure of the entire set of
+section variables occurring in the statement.
+
+
+.. cmdv:: Proof using -(@ident1 ... @identn).
+
+Use all section variables except :n:`@ident1` ... :n:`@identn`.
+
+
+.. cmdv:: Proof using @collection1 + @collection2 .
+
+
+.. cmdv:: Proof using @collection1 - @collection2 .
+
+
+.. cmdv:: Proof using @collection - ( @ident1 ... @identn ).
+
+
+.. cmdv:: Proof using @collection * .
+
+Use section variables being, respectively, in the set union, set
+difference, set complement, set forward transitive closure. See
+Section :ref:`nameaset` to know how to form a named collection. The ``*`` operator
+binds stronger than ``+`` and ``-``.
+
+
+Proof using options
+```````````````````
+
+The following options modify the behavior of ``Proof using``.
+
+
+.. cmdv:: Set Default Proof Using "@expression".
+
+Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default
+Proof Using "a b"``. will complete all ``Proof`` commands not followed by a
+using part with using ``a`` ``b``.
+
+
+.. cmdv:: Set Suggest Proof Using.
+
+When ``Qed`` is performed, suggest a using annotation if the user did not
+provide one.
+
+..  _`nameaset`:
+
+Name a set of section hypotheses for ``Proof using``
+````````````````````````````````````````````````````
+
+The command ``Collection`` can be used to name a set of section
+hypotheses, with the purpose of making ``Proof using`` annotations more
+compact.
+
+
+.. cmdv:: Collection Some := x y z.
+
+Define the collection named "Some" containing ``x``, ``y`` and ``z``.
+
+
+.. cmdv:: Collection Fewer := Some - z.
+
+Define the collection named "Fewer" containing only ``x`` and ``y``.
+
+
+.. cmdv::  Collection Many := Fewer + Some.
+.. cmdv::  Collection Many := Fewer - Some.
+
+Define the collection named "Many" containing the set union or set
+difference of "Fewer" and "Some".
+
+
+.. cmdv:: Collection Many := Fewer - (x y).
+
+Define the collection named "Many" containing the set difference of
+"Fewer" and the unnamed collection ``x`` ``y``.
+
+
+.. cmd:: Abort.
+
+This command cancels the current proof development, switching back to
+the previous proof development, or to the |Coq| toplevel if no other
+proof was edited.
+
+
+.. exn:: No focused proof (No proof-editing in progress)
+
+
+
+.. cmdv::  Abort @ident.
+
+Aborts the editing of the proof named :n:`@ident`.
+
+.. cmdv:: Abort All.
+
+Aborts all current goals, switching back to the |Coq|
+toplevel.
+
+
+
+.. cmd:: Existential @num := @term.
+
+This command instantiates an existential variable. :n:`@num` is an index in
+the list of uninstantiated existential variables displayed by ``Show
+Existentials`` (described in Section :ref:`requestinginformation`).
+
+This command is intended to be used to instantiate existential
+variables when the proof is completed but some uninstantiated
+existential variables remain. To instantiate existential variables
+during proof edition, you should use the tactic instantiate.
+
+
+See also: ``instantiate (num:= term).`` in Section
+:ref:`TODO-controllingtheproofflow`.
+See also: ``Grab Existential Variables.`` below.
+
+
+.. cmd:: Grab Existential Variables.
+
+This command can be run when a proof has no more goal to be solved but
+has remaining uninstantiated existential variables. It takes every
+uninstantiated existential variable and turns it into a goal.
+
+
+Navigation in the proof tree
+--------------------------------
+
+
+.. cmd:: Undo.
+
+This command cancels the effect of the last command. Thus, it
+backtracks one step.
+
+
+.. cmdv:: Undo @num.
+
+Repeats Undo :n:`@num` times.
+
+.. cmdv:: Restart.
+
+This command restores the proof editing process to the original goal.
+
+
+.. exn:: No focused proof to restart
+
+
+.. cmd:: Focus.
+
+This focuses the attention on the first subgoal to prove and the
+printing of the other subgoals is suspended until the focused subgoal
+is solved or unfocused. This is useful when there are many current
+subgoals which clutter your screen.
+
+
+.. cmdv:: Focus @num.
+
+This focuses the attention on the :n:`@num` th subgoal to
+prove.
+
+*This command is deprecated since 8.8*: prefer the use of bullets or
+focusing brackets instead, including :n:`@num : %{`
+
+.. cmd:: Unfocus.
+
+This command restores to focus the goal that were suspended by the
+last ``Focus`` command.
+
+*This command is deprecated since 8.8.*
+
+.. cmd:: Unfocused.
+
+Succeeds if the proof is fully unfocused, fails is there are some
+goals out of focus.
+
+
+.. cmd:: %{ %| %}
+
+The command ``{`` (without a terminating period) focuses on the first
+goal, much like ``Focus.`` does, however, the subproof can only be
+unfocused when it has been fully solved ( *i.e.* when there is no
+focused goal left). Unfocusing is then handled by ``}`` (again, without a
+terminating period). See also example in next section.
+
+Note that when a focused goal is proved a message is displayed
+together with a suggestion about the right bullet or ``}`` to unfocus it
+or focus the next one.
+
+.. cmdv:: @num: %{
+
+This focuses on the :n:`@num` th subgoal to prove.
+
+Error messages:
+
+.. exn:: This proof is focused, but cannot be unfocused this way
+
+You are trying to use ``}`` but the current subproof has not been fully solved.
+
+.. exn:: No such goal
+
+.. exn:: Brackets only support the single numbered goal selector
+
+
+See also error messages about bullets below.
+
+Bullets
+```````
+
+Alternatively to ``{`` and ``}``, proofs can be structured with bullets. The
+use of a bullet ``b`` for the first time focuses on the first goal ``g``, the
+same bullet cannot be used again until the proof of ``g`` is completed,
+then it is mandatory to focus the next goal with ``b``. The consequence is
+that ``g`` and all goals present when ``g`` was focused are focused with the
+same bullet ``b``. See the example below.
+
+Different bullets can be used to nest levels. The scope of bullet does
+not go beyond enclosing ``{`` and ``}``, so bullets can be reused as further
+nesting levels provided they are delimited by these. Available bullets
+are ``-``, ``+``, ``*``, ``--``, ``++``, ``**``, ``---``, ``+++``, ``***``, ... (without a terminating period).
+
+Note again that when a focused goal is proved a message is displayed
+together with a suggestion about the right bullet or ``}`` to unfocus it
+or focus the next one.
+
+.. note::
+
+   In Proof General (``Emacs`` interface to |Coq|), you must use
+   bullets with the priority ordering shown above to have a correct
+   indentation. For example ``-`` must be the outer bullet and ``**`` the inner
+   one in the example below.
+
+The following example script illustrates all these features:
+
+.. example::
+  .. coqtop:: all
+
+    Goal (((True /\ True) /\ True) /\ True) /\ True.
+    Proof.
+    split.
+    - split.
+    + split.
+    ** { split.
+    - trivial.
+    - trivial.
+    }
+    ** trivial.
+    + trivial.
+    - assert True.
+    { trivial. }
+    assumption.
+
+
+.. exn:: Wrong bullet @bullet1 : Current bullet @bullet2 is not finished.
+
+Before using bullet :n:`@bullet1` again, you should first finish proving the current focused goal. Note that :n:`@bullet1` and :n:`@bullet2` may be the same.
+
+.. exn:: Wrong bullet @bullet1 : Bullet @bullet2 is mandatory here.
+
+You must put :n:`@bullet2` to focus next goal. No other bullet is allowed here.
+
+.. exn:: No such goal. Focus next goal with bullet @bullet.
+
+You tried to applied a tactic but no goal where under focus. Using :n:`@bullet` is  mandatory here.
+
+.. exn:: No such goal. Try unfocusing with %{.
+
+You just finished a goal focused by ``{``, you must unfocus it with ``}``.
+
+Set Bullet Behavior
+```````````````````
+
+The bullet behavior can be controlled by the following commands.
+
+.. opt:: Bullet Behavior "None".
+
+This makes bullets inactive.
+
+.. opt:: Bullet Behavior "Strict Subproofs".
+
+This makes bullets active (this is the default behavior).
+
+
+
+Requesting information
+----------------------
+
+
+.. cmd:: Show.
+
+This command displays the current goals.
+
+
+.. cmdv:: Show @num
+
+Displays only the :n:`@num`-th subgoal.
+
+.. exn:: No such goal
+.. exn:: No focused proof
+
+.. cmdv:: Show @ident.
+
+Displays the named goal :n:`@ident`. This is useful in
+particular to display a shelved goal but only works if the
+corresponding existential variable has been named by the user
+(see :ref:`exvariables`) as in the following example.
+
+.. example::
+
+  .. coqtop:: all
+
+    Goal exists n, n = 0.
+    eexists ?[n].
+    Show n.
+
+.. cmdv:: Show Script.
+
+Displays the whole list of tactics applied from the
+beginning of the current proof. This tactics script may contain some
+holes (subgoals not yet proved). They are printed under the form
+
+``<Your Tactic Text here>``.
+
+.. cmdv:: Show Proof.
+
+It displays the proof term generated by the tactics
+that have been applied. If the proof is not completed, this term
+contain holes, which correspond to the sub-terms which are still to be
+constructed. These holes appear as a question mark indexed by an
+integer, and applied to the list of variables in the context, since it
+may depend on them. The types obtained by abstracting away the context
+from the type of each hole-placer are also printed.
+
+.. cmdv:: Show Conjectures.
+
+It prints the list of the names of all the
+theorems that are currently being proved. As it is possible to start
+proving a previous lemma during the proof of a theorem, this list may
+contain several names.
+
+.. cmdv:: Show Intro.
+
+If the current goal begins by at least one product,
+this command prints the name of the first product, as it would be
+generated by an anonymous ``intro``. The aim of this command is to ease
+the writing of more robust scripts. For example, with an appropriate
+Proof General macro, it is possible to transform any anonymous ``intro``
+into a qualified one such as ``intro y13``. In the case of a non-product
+goal, it prints nothing.
+
+.. cmdv:: Show Intros.
+
+This command is similar to the previous one, it
+simulates the naming process of an intros.
+
+.. cmdv:: Show Existentials.
+
+It displays the set of all uninstantiated
+existential variables in the current proof tree, along with the type
+and the context of each variable.
+
+.. cmdv:: Show Match @ident.
+
+This variant displays a template of the Gallina
+``match`` construct with a branch for each constructor of the type
+:n:`@ident`
+
+.. example::
+  .. coqtop:: all
+
+     Show Match nat.
+
+.. exn:: Unknown inductive type
+
+.. exn:: Show Universes.
+
+It displays the set of all universe constraints and
+its normalized form at the current stage of the proof, useful for
+debugging universe inconsistencies.
+
+
+.. cmd:: Guarded.
+
+Some tactics (e.g. refine :ref:`applyingtheorems`) allow to build proofs using
+fixpoint or co-fixpoint constructions. Due to the incremental nature
+of interactive proof construction, the check of the termination (or
+guardedness) of the recursive calls in the fixpoint or cofixpoint
+constructions is postponed to the time of the completion of the proof.
+
+The command ``Guarded`` allows checking if the guard condition for
+fixpoint and cofixpoint is violated at some time of the construction
+of the proof without having to wait the completion of the proof.
+
+
+Controlling the effect of proof editing commands
+------------------------------------------------
+
+
+.. opt:: Hyps Limit @num.
+
+This option controls the maximum number of hypotheses displayed in goals
+after the application of a tactic. All the hypotheses remain usable
+in the proof development.
+When unset, it goes back to the default mode which is to print all
+available hypotheses.
+
+
+.. opt:: Automatic Introduction.
+
+This option controls the way binders are handled
+in assertion commands such as ``Theorem ident [binders] : form``. When the
+option is set, which is the default, binders are automatically put in
+the local context of the goal to prove.
+
+The option can be unset by issuing ``Unset Automatic Introduction``. When
+the option is unset, binders are discharged on the statement to be
+proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be
+used to move the assumptions to the local context.
+
+
+Controlling memory usage
+------------------------
+
+When experiencing high memory usage the following commands can be used
+to force |Coq| to optimize some of its internal data structures.
+
+
+.. cmd:: Optimize Proof.
+
+This command forces |Coq| to shrink the data structure used to represent
+the ongoing proof.
+
+
+.. cmd:: Optimize Heap.
+
+This command forces the |OCaml| runtime to perform a heap compaction.
+This is in general an expensive operation.
+See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
+There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`)
diff --git a/doc/tools/coqrst/notations/TacticNotations.g b/doc/tools/coqrst/notations/TacticNotations.g
index 5176c51d28..68658fe491 100644
--- a/doc/tools/coqrst/notations/TacticNotations.g
+++ b/doc/tools/coqrst/notations/TacticNotations.g
@@ -26,7 +26,7 @@ hole: ID;
 LGROUP: '{' [+*?];
 LBRACE: '{';
 RBRACE: '}';
-METACHAR: '%' [|()];
+METACHAR: '%' [|(){}];
 ATOM: '@' | ~[@{} ]+;
 ID: '@' [a-zA-Z0-9_]+;
 WHITESPACE: ' '+;
diff --git a/doc/tools/coqrst/notations/TacticNotationsLexer.py b/doc/tools/coqrst/notations/TacticNotationsLexer.py
index ffa774b9ba..61d8d2f9e6 100644
--- a/doc/tools/coqrst/notations/TacticNotationsLexer.py
+++ b/doc/tools/coqrst/notations/TacticNotationsLexer.py
@@ -12,19 +12,19 @@ def serializedATN():
         buf.write("\4\b\t\b\3\2\3\2\3\2\3\3\3\3\3\4\3\4\3\5\3\5\3\5\3\6\3")
         buf.write("\6\6\6\36\n\6\r\6\16\6\37\5\6\"\n\6\3\7\3\7\6\7&\n\7\r")
         buf.write("\7\16\7\'\3\b\6\b+\n\b\r\b\16\b,\2\2\t\3\3\5\4\7\5\t\6")
-        buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+~~\6\2\"\"BB}}\177\177")
-        buf.write("\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3\2\2")
-        buf.write("\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2\2\3")
-        buf.write("\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2\13")
-        buf.write("!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23\t")
-        buf.write("\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27\7")
-        buf.write("\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32\n")
-        buf.write("\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36\37")
-        buf.write("\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3\2")
-        buf.write("\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3\2")
-        buf.write("\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+\7")
-        buf.write("\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3\2")
-        buf.write("\2\2\7\2\37!\',\2")
+        buf.write("\13\7\r\b\17\t\3\2\6\4\2,-AA\4\2*+}\177\6\2\"\"BB}}\177")
+        buf.write("\177\6\2\62;C\\aac|\2\61\2\3\3\2\2\2\2\5\3\2\2\2\2\7\3")
+        buf.write("\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r\3\2\2\2\2\17\3\2\2")
+        buf.write("\2\3\21\3\2\2\2\5\24\3\2\2\2\7\26\3\2\2\2\t\30\3\2\2\2")
+        buf.write("\13!\3\2\2\2\r#\3\2\2\2\17*\3\2\2\2\21\22\7}\2\2\22\23")
+        buf.write("\t\2\2\2\23\4\3\2\2\2\24\25\7}\2\2\25\6\3\2\2\2\26\27")
+        buf.write("\7\177\2\2\27\b\3\2\2\2\30\31\7\'\2\2\31\32\t\3\2\2\32")
+        buf.write("\n\3\2\2\2\33\"\7B\2\2\34\36\n\4\2\2\35\34\3\2\2\2\36")
+        buf.write("\37\3\2\2\2\37\35\3\2\2\2\37 \3\2\2\2 \"\3\2\2\2!\33\3")
+        buf.write("\2\2\2!\35\3\2\2\2\"\f\3\2\2\2#%\7B\2\2$&\t\5\2\2%$\3")
+        buf.write("\2\2\2&\'\3\2\2\2\'%\3\2\2\2\'(\3\2\2\2(\16\3\2\2\2)+")
+        buf.write("\7\"\2\2*)\3\2\2\2+,\3\2\2\2,*\3\2\2\2,-\3\2\2\2-\20\3")
+        buf.write("\2\2\2\7\2\37!\',\2")
         return buf.getvalue()
 
 
diff --git a/doc/tools/coqrst/notations/html.py b/doc/tools/coqrst/notations/html.py
index 44212d7889..9c94a4b2d7 100644
--- a/doc/tools/coqrst/notations/html.py
+++ b/doc/tools/coqrst/notations/html.py
@@ -43,7 +43,11 @@ class TacticNotationsToHTMLVisitor(TacticNotationsVisitor):
         tags.span(ctx.ID().getText()[1:], _class="hole")
 
     def visitMeta(self, ctx:TacticNotationsParser.MetaContext):
-        tags.span(ctx.METACHAR().getText()[1:], _class="meta")
+        txt = ctx.METACHAR().getText()[1:]
+        if (txt == "{") or (txt == "}"):
+            tags.span(txt)
+        else:
+            tags.span(txt, _class="meta")
 
     def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext):
         tags.span(" ")          # TODO: no need for a <span> here