Port ssr manual to Coq's latex/hevea style

Work done by Assia Mahboubi and Enrico Tassi

6 files changed, 5080 insertions, 13 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 1fed4ee7b..dd7717359 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -62,7 +62,7 @@ REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
   RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
   RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \
-  AsyncProofs.tex ) \
+  AsyncProofs.tex RefMan-ssr.tex) \
   $(REFMANCOQTEXFILES) \
 
 REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps
diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css
index 5df2ae2eb..32c0b3316 100644
--- a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css
+++ b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css
@@ -522,6 +522,19 @@ td.menu-disabled,td.menu-disabled a
 	border:1px solid #ccc;
 }
 
+.lstlisting {
+    display: block;
+    font-family: monospace;
+    white-space: pre;
+    margin: 1em 0;
+}
+.center {
+    text-align: center;
+}
+.centered {
+    display: block-inline;
+}
+
 /*----------download table------------*/
 
 table.downloadtable
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 96fb1eb75..6ec333c80 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -558,7 +558,7 @@ $\Sort$ is called the sort of the inductive type $t$.
 \paragraph{Examples}
 
     \newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
-    \begin{array}{r @{\mathrm{~:=~}} l}
+    \begin{array}{r@{\mathrm{~:=~}}l}
       #2 & #3 \\
     \end{array}
     \hskip-.4em
@@ -569,7 +569,7 @@ The declaration for parameterized lists is:
 \begin{latexonly}
     \vskip.5em
 
-\ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r \colon l}
+    \ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r@{:}l}
                                       \Nil & \forall A:\Set,\List~A \\
                                       \cons & \forall A:\Set, A \ra \List~A \ra \List~A
                                    \end{array}
@@ -613,8 +613,8 @@ Inductive list (A:Set) : Set :=
 \noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is:
 \begin{latexonly}
     \vskip.5em
-\ind{~}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
-       {\left[\begin{array}{r \colon l}
+\ind{~}{\left[\begin{array}{r@{:}l}\tree&\Set\\\forest&\Set\end{array}\right]}
+    {\left[\begin{array}{r@{:}l}
              \node & \forest \ra \tree\\
              \emptyf & \forest\\
              \consf & \tree \ra \forest \ra \forest\\
@@ -680,15 +680,15 @@ with forest : Set :=
 
 \noindent The declaration for a mutual inductive definition of {\even} and {\odd} is:
 \begin{latexonly}
-    \newcommand\GammaI{\left[\begin{array}{r \colon l}
-                        \even & \nat\ra\Prop \\
-                        \odd & \nat\ra\Prop
+	\newcommand\GammaI{\left[\begin{array}{r@{:}l}
+			    \even & \nat\ra\Prop \\
+			    \odd & \nat\ra\Prop
                       \end{array}
                 \right]}
-    \newcommand\GammaC{\left[\begin{array}{r \colon l}
-                        \evenO & \even~\nO \\
-                        \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)\\
-                        \oddS & \forall n : \nat, \even~n \ra \odd~(\nS~n)
+		\newcommand\GammaC{\left[\begin{array}{r@{:}l}
+			    \evenO & \even~\nO \\
+			    \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)\\
+			    \oddS & \forall n : \nat, \even~n \ra \odd~(\nS~n)
                       \end{array}
                 \right]}
     \vskip.5em
@@ -769,7 +769,7 @@ Provided that our environment $E$ contains inductive definitions we showed befor
 these two inference rules above enable us to conclude that:
 \vskip.5em
 \newcommand\prefix{E[\Gamma]\vdash\hskip.25em}
-$\begin{array}{@{} l}
+$\begin{array}{@{}l}
    \prefix\even : \nat\ra\Prop\\
    \prefix\odd : \nat\ra\Prop\\
    \prefix\evenO : \even~\nO\\
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
new file mode 100644
index 000000000..0e49520bf
--- /dev/null
+++ b/doc/refman/RefMan-ssr.tex
@@ -0,0 +1,4886 @@
+\achapter{The SSReflect proof language}
+\aauthor{Georges Gonthier, Assia Mahboubi, Enrico Tassi}
+
+\newcommand{\ssr}{{\sc SSReflect}}
+
+% listing
+\ifhevea\newcommand{\ssrC}[1]{\texttt{#1}}\else\newcommand{\ssrC}[1]{\text{\lstinline!#1!}}\fi
+\ifhevea\renewenvironment{center}{\@open{div}{class="center"}\@open{div}{class="centered"}}{\@close{div}\@close{div}}\fi
+% non-terminal
+%\newcommand\ssrN[2][]{\ensuremath{\langle\mbox{\itshape\rmfamily\small #2}\rangle_{#1}}}
+\newcommand\ssrN[2][]{{\textsl {#2}}\ensuremath{_{#1}}}
+\ifhevea\newcommand{\underbar}[1]{\underline{#1}}\fi
+
+% TODO: only use \ssrC
+\let\ssrL=\lstinline
+
+\newcommand{\iitem}{{\it i-item}}
+\newcommand{\ditem}{{\it d-item}}
+\newcommand{\optional}[1]{{\it[}#1{\it]}}
+\newcommand{\optsep}{{\it|}}
+\newcommand{\idx}[1]{\tacindex{#1 (ssreflect)}}
+\newcommand{\idxC}[1]{\comindex{#1 (ssreflect)}}
+
+\newenvironment{new}%
+  {\begin{Sbox}\begin{minipage}{0.97\textwidth}%
+    \begin{flushright}\textcolor{red}{\fbox{Version 1.3}}%
+      \end{flushright}\noindent}%
+  {\end{minipage}\end{Sbox}\noindent\doublebox{\TheSbox}}
+\section{Introduction}\label{sec:intro}
+
+This chapter describes an extension to the \Coq{} tactic language,
+originally designed to provide support at the tactic level for the
+so-called \emph{small scale reflection} proof methodology.
+% \marginpar{Provide a citation here?} TODO: cite mcb
+However, its tactics and tacticals
+provide features of general interest for a wide audience of users.
+
+In particular:
+\begin{itemize}
+\item support for forward steps (see the \ssrC{have}, \ssrC{generally have}, \ssrC{without loss} and \ssrC{suffices} tactics~\ref{sssec:have,ssec:wlog})
+\item support for bookkeeping (see the \ssrC{:}, \ssrC{=>} and \ssrC{in} tacticals~\ref{ssec:profstack,ssec:gloc})
+\item common support for subterm selection in all tactics that deal with subterms
+	(see the term selection language~\ref{ssec:rewp})
+\item unified interface for rewriting, definition expansion, and
+	partial evaluation (see the \ssrC{rewrite} tactic~\ref{sec:rw})
+\item support for so-called reflection steps (via \emph{views}~\ref{sec:views})
+\end{itemize}
+
+In fact, only the last functionality is specific to small-scale
+reflection. All the others are of general use.
+
+\iffalse
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{How to read this documentation}
+
+The syntax of the tactics is presented as follows:
+\begin{itemize}
+\item \ssrC{terminals} are in typewriter font and \ssrN{non terminals} are
+  between angle brackets.
+\item Optional parts of the grammar are surrounded by \optional{ }
+  brackets. These should not be confused with verbatim brackets
+  \ssrC{[ ]}, which are delimiters in the \ssr{} syntax.
+\item A vertical rule {\optsep} indicates an alternative in the syntax, and
+  should not be confused with a
+  verbatim vertical rule between verbatim brackets \ssrC{[ | ]}.
+\item A non empty list of non terminals (at least one item should be
+  present) is represented by \ssrN{non terminals}$^+$. A possibly empty
+  one is represented by \ssrN{non terminals}$^*$.
+\item In a non empty list of non terminals, items are separated by blanks.
+\end{itemize}
+\fi
+
+% Hevea has no colors
+\ifhevea \else
+\noindent We follow the default color scheme of the \ssr{} mode for
+ProofGeneral provided in the distribution:
+
+\centerline{
+\textcolor{dkblue}{\texttt{tactic}} or \textcolor{dkviolet}{\tt
+  Command} or \textcolor{dkgreen}{\tt keyword} or
+\textcolor{dkpink}{\tt tactical}}
+
+\noindent Closing tactics/tacticals like \ssrC{exact} or \ssrC{by} (see section
+\ref{ssec:termin}) are in red.
+\fi
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Acknowledgments}
+The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier
+and Laurence Rideau for their comments and suggestions.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newpage\section{Usage}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Getting started}\label{sec:files}
+The present manual describes the behavior of
+the \ssr{} extension after having loaded a minimal set of libraries:
+{\tt ssreflect.v}, {\tt ssrfun.v} and {\tt ssrbool.v} and a few options set.
+
+\begin{lstlisting}
+  From Coq Require Import ssreflect ssrfun ssrbool.
+  Set Implicit Arguments.
+  Unset Strict Implicit.
+  Unset Printing Implicit Defensive.
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Compatibility issues}\label{sec:compat}
+Every effort has been made to make the small-scale reflection
+extensions upward compatible with the rest of \Coq{}, but a few
+discrepancies were unavoidable:
+\begin{itemize}
+\item New keywords (\ssrC{is}) might clash with variable, constant,
+tactic or tactical names, or with quasi-keywords in tactic or
+vernacular notations.
+\item New tactic(al)s names (\ssrC{last}, \ssrC{done}, \ssrC{have},
+  \ssrC{suffices}, \ssrC{suff},
+  \ssrC{without loss}, \ssrC{wlog}, \ssrC{congr}, \ssrC{unlock}) might clash
+  with user tactic names.
+\item Identifiers with both leading and trailing \ssrC{_}, such as \ssrC{_x_},
+are reserved by \ssr{} and cannot appear in scripts.
+\item The extensions to the \ssrC{rewrite} tactic are partly
+incompatible with those available in current versions of \Coq{};
+in particular:
+\ssrC{rewrite .. in (type of k)} or \\ \ssrC{rewrite .. in *} or any other
+variant of \ssrC{rewrite} will not work, and the \ssr{} syntax and semantics for occurrence selection and
+rule chaining is different.
+
+Use an explicit rewrite direction (\ssrC{rewrite <-} $\dots$ or \ssrC{rewrite ->} $\dots$)
+to access the \Coq{} \ssrC{rewrite} tactic.
+\item New symbols (\ssrC{//, /=, //=}) might clash with adjacent existing
+  symbols (e.g., '\ssrC{//}') instead of '\ssrC{/}''\ssrC{/}'). This can be avoided
+  by inserting white spaces.
+\item New constant and theorem names might clash with the user
+theory. This can be avoided by not importing all of \ssr{}:
+\begin{lstlisting}
+  From Coq Require ssreflect.
+  Import ssreflect.SsrSyntax.
+\end{lstlisting}
+Note that \ssr{}'s extended rewrite syntax and reserved identifiers are
+enabled only if the \ssrC{ssreflect} module has been required and if
+\ssrC{SsrSyntax} has been imported. Thus a file that requires (without importing)
+ \ssrC{ssreflect} and imports \ssrC{SsrSyntax}, can be
+required and imported without automatically enabling \ssr{}'s
+extended rewrite syntax and reserved identifiers.
+\item Some user notations (in particular, defining an infix ';') might
+interfere with the "open term", parenthesis free, syntax of tactics
+such as \ssrC{have}, \ssrC{set} and \ssrC{pose}.
+\item The generalization of \ssrC{if} statements to non-Boolean
+conditions is turned off by \ssr{}, because it is mostly subsumed by
+\ssrC{Coercion} to \ssrC{bool} of the \ssrC{sum}XXX types (declared in
+\ssrC{ssrfun.v})
+and the \ssrC{if} {\term} \ssrC{is} \ssrN{pattern} \ssrC{then} {\term} \ssrC{else} {\term} construct (see
+\ref{ssec:patcond}). To use the generalized form, turn off the \ssr{}
+Boolean \ssrC{if} notation using the command:
+\begin{lstlisting}
+  Close Scope boolean_if_scope.
+\end{lstlisting}
+\item The following two options can be unset to disable the
+      incompatible \ssrC{rewrite} syntax and allow
+      reserved identifiers to appear in scripts.
+\begin{lstlisting}
+  Unset SsrRewrite.
+  Unset SsrIdents.
+\end{lstlisting}
+\end{itemize}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Gallina extensions}
+
+Small-scale reflection makes an extensive use of the programming
+subset of Gallina, \Coq{}'s logical specification language. This subset
+is quite suited to the description of functions on representations,
+because it closely follows the well-established design of the ML
+programming language.The \ssr{} extension provides three additions
+to Gallina, for pattern assignment, pattern testing, and polymorphism;
+these mitigate minor but annoying discrepancies between Gallina and ML.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Pattern assignment}\label{ssec:patass}
+The \ssr{} extension provides the following construct for
+irrefutable pattern matching, that is, destructuring assignment:
+
+\ssrC{let: } \ssrN{pattern}  \ssrC{:=} \ssrN[1]{term} \ssrC{in} \ssrN[2]{term}
+
+Note the colon `\ssrC{:}' after the \ssrC{let} keyword, which avoids any
+ambiguity with a function
+definition or \Coq{}'s basic destructuring \ssrC{let}. The \ssrC{let:}
+construct differs from the latter in that
+\begin{itemize}
+\item The pattern can be nested (deep pattern matching), in
+  particular, this allows expression of the form:
+\begin{lstlisting}
+ let: exist (x, y) p_xy := Hp in ...
+\end{lstlisting}
+\item The destructured constructor is explicitly given in the
+  pattern, and is used for type inference, e.g.,
+\begin{lstlisting}
+  Let f u := let: (m, n) := u in m + n.
+\end{lstlisting}
+using a colon \ssrC{let:}, infers \ssrC{f : nat * nat -> nat}, whereas
+\begin{lstlisting}
+  Let f u := let (m, n) := u in m + n.
+\end{lstlisting}
+with a usual \ssrC{let}, requires an extra type annotation.
+\end{itemize}
+The \ssrC{let:} construct is just (more legible) notation for the primitive Gallina expression
+
+\begin{center}
+\ssrC{match} \ssrN[1]{term} \ssrC{with} \ssrN{pattern} \ssrC{=>} \ssrN[2]{term} \ssrC{end}
+\end{center}
+
+The \ssr{} destructuring assignment supports all the dependent match
+annotations; the  full syntax is
+
+\begin{center}
+\ssrC{let:} \ssrN[1]{pattern} \ssrC{as} \ssrN{ident} \ssrC{in} \ssrN[2]{pattern} \ssrC{:=} \ssrN[1]{term} \ssrC{return} \ssrN[2]{term} \ssrC{in} \ssrN[3]{term}
+\end{center}
+
+where \ssrN[2]{pattern} is a \emph{type} pattern and \ssrN[1]{term} and
+\ssrN[2]{term} are types.
+
+When the \ssrC{as} and \ssrC{return} are both present, then \ssrN{ident} is bound
+in both the type \ssrN[2]{term} and the expression \ssrN[3]{term};
+variables in the optional type pattern \ssrN[2]{pattern} are
+bound only in the type \ssrN[2]{term}, and other variables in \ssrN[1]{pattern} are
+bound only in the expression \ssrN[3]{term}, however.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Pattern conditional}\label{ssec:patcond}
+The following construct can be used for a refutable pattern matching,
+that is, pattern testing:
+
+\begin{center}
+\ssrC{if}\ \ssrN[1]{term} \ssrC{is} \ssrN[1]{pattern} \ssrC{then} \ssrN[2]{term} \ssrC{else} \ssrN[3]{term}
+\end{center}
+
+Although this construct is not strictly ML (it does exits in variants
+such as the pattern calculus or the $\rho$-calculus), it turns out to be
+very convenient for writing functions on representations,
+because most such functions manipulate simple datatypes such as Peano
+integers, options,
+lists, or binary trees, and the pattern conditional above is almost
+always the right construct
+for analyzing such simple types. For example, the \ssrC{null} and
+\ssrC{all} list function(al)s can be defined as follows:
+\begin{lstlisting}
+  Variable d: Set.
+  Fixpoint |*null*| (s : list d) := if s is nil then true else false.
+  Variable a : d -> bool.
+  Fixpoint |*all*| (s : list d) : bool :=
+     if s is cons x s' then a x && all s' else true.
+\end{lstlisting}
+
+The pattern conditional also provides a notation for destructuring
+assignment with a refutable pattern, adapted to the pure functional
+setting of Gallina, which lacks a \\\texttt{Match\_Failure} exception.
+
+Like \ssrC{let:} above, the \ssrC{if}$\dots$\ssrC{is} construct is just (more legible)
+notation for the primitive Gallina expression:
+
+\begin{center}
+\ssrC{match} \ssrN[1]{term} \ssrC{with} \ssrN{pattern} \ssrC{=>} \ssrN[2]{term} \ssrC{| _ =>} \ssrN[2]{term} \ssrC{end}
+\end{center}
+
+Similarly, it will always be displayed as the expansion of this form
+in terms of primitive \ssrC{match} expressions (where the default
+expression $\ssrN[3]{term}$ may be replicated).
+
+
+Explicit pattern testing also largely subsumes the generalization of
+the \ssrC{if} construct to all binary datatypes; compare:
+
+\begin{center}
+\ssrC{if} {\term} \ssrC{is inl _ then} \ssrN[l]{term} \ssrC{else} \ssrN[r]{term}
+\end{center}
+
+and:
+
+\begin{center}
+\ssrC{if} {\term} \ssrC{then} \ssrN[l]{term} \ssrC{else} \ssrN[r]{term}
+\end{center}
+
+The latter appears to be marginally shorter, but it is quite
+ambiguous, and indeed often
+requires an explicit annotation term : \ssrC{\{_\}+\{_\}} to type-check,
+which evens the character count.
+
+Therefore, \ssr{} restricts by default the condition of a plain \ssrC{if}
+construct to the standard \ssrC{bool} type; this avoids spurious type
+annotations, e.g., in:
+\begin{lstlisting}
+  Definition |*orb*| b1 b2 := if b1 then true else b2.
+\end{lstlisting}
+As pointed out in section~\ref{sec:compat}, this restriction can be removed with
+the command:
+\begin{lstlisting}
+  Close Scope boolean_if_scope.
+\end{lstlisting}
+Like \ssrC{let:} above, the \ssrC{if} {\term} \ssrC{is} \ssrN{pattern}
+\ssrC{else} {\term} construct
+supports the dependent \ssrC{match} annotations:
+
+\begin{center}
+\ssrC{if} \ssrN[1]{term} \ssrC{is} \ssrN[1]{pattern} \ssrC{as} \ssrN{ident} \ssrC{in} \ssrN[2]{pattern} \ssrC{return} \ssrN[2]{term} \ssrC{then} \ssrN[3]{term} \ssrC{else} \ssrN[4]{term}
+\end{center}
+
+As in \ssrC{let:} the variable \ssrN{ident} (and those in
+the type pattern \ssrN[2]{pattern}) are bound in \ssrN[2]{term}; \ssrN{ident} is
+also bound in \ssrN[3]{term} (but not in \ssrN[4]{term}), while the
+variables in \ssrN[1]{pattern} are bound only in \ssrN[3]{term}.
+
+\noindent
+Another variant allows to treat the else case first:
+
+\begin{center}
+\ssrC{if} \ssrN[1]{term} \ssrC{isn't} \ssrN[1]{pattern} \ssrC{then} \ssrN[2]{term} \ssrC{else} \ssrN[3]{term}
+\end{center}
+
+Note that \ssrN[1]{pattern} eventually binds variables in \ssrN[3]{term}
+and not \ssrN[2]{term}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Parametric polymorphism}\label{ssec:parampoly}
+
+Unlike ML, polymorphism in core Gallina is explicit: the type
+parameters of polymorphic  functions must be declared explicitly, and
+supplied at each point of use. However, \Coq{} provides two features
+to suppress redundant parameters:
+\begin{itemize}
+\item Sections are used to provide (possibly implicit) parameters for
+  a set of definitions.
+\item Implicit arguments declarations are used to tell \Coq{} to use
+  type inference to deduce some parameters from the context at each
+  point of call.
+\end{itemize}
+The combination of these features provides a fairly good emulation of ML-style
+polymorphism, but unfortunately this emulation breaks down for
+higher-order programming. Implicit arguments are indeed not inferred
+at all points of use, but only at
+points of call, leading to  expressions such as
+\begin{lstlisting}
+  Definition |*all_null*| (s : list T) := all (@null T) s.
+\end{lstlisting}
+Unfortunately, such higher-order expressions are quite frequent in
+representation functions, especially those which use \Coq{}'s
+\ssrC{Structure}s to emulate Haskell type classes.
+
+Therefore, \ssr{} provides a variant of \Coq{}'s implicit argument
+declaration, which  causes \Coq{} to fill in some implicit parameters
+at each point of use, e.g., the above definition can be written:
+\begin{lstlisting}
+  Definition |*all_null*| (s : list d) := all null s.
+\end{lstlisting}
+Better yet, it can be omitted entirely, since \ssrC{all_null s} isn't
+much of an improvement over \ssrC{all null s}.
+
+The syntax of the new declaration is
+
+\begin{center}
+\ssrC{Prenex Implicits} \ssrN{ident}$^+$.
+\end{center}
+
+Let us denote $_1 \dots c_n$ the list of identifiers given to a
+\ssrC{Prenex Implicits} command.
+The command checks that each $c_i$ is the name of a functional
+constant, whose implicit arguments are prenex, i.e., the first $n_i >
+0$ arguments of $c_i$ are implicit; then it assigns
+\ssrC{Maximal Implicit} status to these arguments.
+
+As these prenex implicit arguments are ubiquitous and have often large
+display strings, it is strongly recommended to change the default
+display settings of \Coq{} so that they are not printed (except after a
+\ssrC{Set Printing All} command).
+All \ssr{} library files thus start with the incantation
+\begin{lstlisting}
+  Set Implicit Arguments.
+  Unset Strict Implicit.
+  Unset Printing Implicit Defensive.
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Anonymous arguments}
+
+When in a definition, the type of a certain argument is mandatory, but
+not its name, one usually use ``arrow'' abstractions for prenex
+arguments, or the \ssrC{(_ : }{\term}\ssrC{)} syntax for inner arguments.
+In \ssr{}, the latter can be replaced by the open syntax `\ssrC{of\ }{\term}'
+or (equivalently)  `\ssrC{& }{\term}', which are both syntactically
+equivalent to a \ssrC{(_ : }{\term}\ssrC{)} expression.
+
+For instance, the usual two-contrsuctor polymorphic type \ssrC{list},
+i.e. the one of the
+standard {\tt List} library, can be defined by the following
+declaration:
+\begin{lstlisting}
+  Inductive list (A : Type) : Type := nil | cons of A & list A.
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Wildcards}\label{ssec:wild}
+
+The terms passed as arguments
+to \ssr{} tactics can contain \emph{holes}, materialized by wildcards
+\ssrC{_}.
+Since \ssr{} allows a more powerful form of type inference for these
+arguments, it enhances the possibilities of using such wildcards.
+These holes are in particular used as a convenient shorthand for
+abstractions, especially in local definitions or type expressions.
+
+Wildcards may be interpreted as abstractions (see for example sections
+\ref{ssec:pose} and \ref{ssec:struct}), or their content can be
+inferred from the whole
+context of the goal (see for example section \ref{ssec:set}).
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Definitions}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Definitions}\label{ssec:pose}
+\idx{pose \dots{} := \dots{}}
+\idx{pose fix \dots{} := \dots{}}
+\idx{pose cofix \dots{} := \dots{}}
+
+The \ssrC{pose} tactic allows to add a defined constant to a
+proof context. \ssr{} generalizes this tactic in several ways.
+In particular, the \ssr{} \ssrC{pose} tactic supports \emph{open syntax}:
+the body of
+the definition does not need surrounding parentheses. For instance:
+\begin{lstlisting}
+  pose t := x + y.
+\end{lstlisting}
+is a valid tactic expression.
+
+The \ssrC{pose} tactic is also improved for the
+local definition of higher order terms.
+Local definitions of functions can use the same syntax as
+global ones. The tactic:
+\begin{lstlisting}
+  pose f x y := x + y.
+\end{lstlisting}
+adds to the context the defined constant:
+\begin{lstlisting}
+  f := fun x y : nat => x + y : nat -> nat -> nat
+\end{lstlisting}
+
+The \ssr{} \ssrC{pose} tactic also supports (co)fixpoints,
+by providing the local counterpart of the
+\ssrC{Fixpoint f := $\dots$ } and \ssrC{CoFixpoint f := $\dots$ } constructs.
+For instance, the following tactic:
+\begin{lstlisting}
+  pose fix f (x y : nat) {struct x} : nat :=
+      if x is S p then S (f p y) else 0.
+\end{lstlisting}
+defines a local fixpoint \ssrC{f}, which mimics the standard \ssrC{plus}
+operation on natural numbers.
+
+Similarly, local cofixpoints can be defined by a tactic of the form:
+\begin{lstlisting}
+  pose cofix f (arg : T) ...
+\end{lstlisting}
+
+The possibility to include wildcards in the body of the definitions
+ offers a smooth
+way of defining local abstractions. The type of ``holes'' is
+guessed by type inference, and the holes are abstracted.
+For instance the tactic:
+\begin{lstlisting}
+  pose f := _ + 1.
+\end{lstlisting}
+is shorthand for:
+\begin{lstlisting}
+  pose f n := n + 1.
+\end{lstlisting}
+
+When the local definition of a function involves both arguments and
+holes, hole abstractions appear first. For instance, the
+tactic:
+\begin{lstlisting}
+  pose f x := x + _.
+\end{lstlisting}
+is shorthand for:
+\begin{lstlisting}
+  pose f n x := x + n.
+\end{lstlisting}
+
+
+The interaction of the \ssrC{pose} tactic with the interpretation of
+implicit arguments results in a powerful and concise syntax for local
+definitions involving dependent types.
+For instance, the tactic:
+\begin{lstlisting}
+  pose f x y := (x, y).
+\end{lstlisting}
+adds to the context the local definition:
+\begin{lstlisting}
+  pose f (Tx Ty : Type) (x : Tx) (y : Ty) := (x, y).
+\end{lstlisting}
+The generalization of wildcards makes the use of the \ssrC{pose} tactic
+resemble ML-like definitions of polymorphic functions.
+
+% The use of \ssrC{Prenex Implicits} declarations (see section
+% \ref{ssec:parampoly}), makes this feature specially convenient.
+% Note that this combines with the interpretation of wildcards, and that
+% it is possible to define:
+% \begin{lstlisting}
+%   pose g x y : prod _ nat := (x, y).
+% \end{lstlisting}
+% which is equivalent to:
+% \begin{lstlisting}
+%   pose g x (y : nat) := (x, y).
+% \end{lstlisting}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Abbreviations}\label{ssec:set}
+\idx{set \dots{} := \dots{}}
+
+
+The \ssr{} \ssrC{set} tactic performs abbreviations: it introduces a
+defined constant for a subterm appearing in the goal and/or in the
+context.
+
+\ssr{} extends the \ssrC{set} tactic by supplying:
+\begin{itemize}
+\item an open syntax, similarly to the \ssrC{pose} tactic;
+\item a more aggressive matching algorithm;
+\item an improved interpretation of wildcards, taking advantage of the
+  matching algorithm;
+\item an improved occurrence selection mechanism allowing to abstract only
+  selected occurrences of a term.
+\end{itemize}
+
+The general syntax of this tactic is
+\begin{center}
+\ssrC{set} \ssrN{ident} \optional{\ssrC{:} \ssrN[1]{term}} \ssrC{:=} \optional{\ssrN{occ-switch}} \ssrN[2]{term}
+\end{center}
+\begin{center}
+\ssrN{occ-switch} ::= \ssrC{\{}[\ssrC{+}|\ssrC{-}] {\naturalnumber}$^*$ \ssrC{\}}
+\end{center}
+
+
+where:
+
+\begin{itemize}
+\item \ssrN{ident} is a fresh identifier chosen by the user.
+\item \ssrN[1]{term} is
+an optional type annotation. The type annotation \ssrN[1]{term} can be
+given in open syntax (no surrounding parentheses). If no \ssrN{occ-switch}
+(described hereafter) is present, it is also
+the case for \ssrN[2]{term}.
+On the other hand, in  presence of \ssrN{occ-switch}, parentheses
+surrounding \ssrN[2]{term} are mandatory.
+\item In the occurrence switch \ssrN{occ-switch}, if the first element
+  of the list is a {\naturalnumber}, this element should be a number, and not
+  an Ltac variable. The empty list \ssrC{\{\}} is not interpreted as a
+  valid occurrence switch.
+\end{itemize}
+% For example, the script:
+% \begin{lstlisting}
+%   Goal forall (f : nat -> nat)(x y : nat), f x + f x = f x.
+%   move=> f x y.
+% \end{lstlisting}
+
+The tactic:
+\begin{lstlisting}
+  set t := f _.
+\end{lstlisting}
+transforms the goal  \ssrC{f x + f x = f x} into \ssrC{t + t = t}, adding
+\ssrC{t := f x} to the context, and the tactic:
+\begin{lstlisting}
+  set t := {2}(f _).
+\end{lstlisting}
+transforms it into \ssrC{f x + t = f x}, adding \ssrC{t := f x} to the context.
+
+The type annotation \ssrN[1]{term} may
+contain wildcards, which will be filled with the appropriate value by
+the matching process.
+
+The tactic first tries to find a subterm of the goal matching
+\ssrN[2]{term} (and its type \ssrN[1]{term}),
+and stops at the first subterm it finds. Then the occurrences
+of this subterm selected by the optional \ssrN{occ-switch} are replaced
+by \ssrN{ident} and a definition \ssrN{ident} \ssrC{:=} {\term} is added to
+the context. If no \ssrN{occ-switch} is present, then all the
+occurrences are abstracted.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Matching}
+
+The matching algorithm compares a pattern \textit{term}
+ with a subterm of the goal by comparing their heads
+and then pairwise unifying their arguments (modulo conversion). Head
+symbols match under the following conditions:
+
+\begin{itemize}
+\item If the head of \textit{term} is a constant, then it
+  should be syntactically equal to the head symbol of the subterm.
+\item If this head is a projection of a canonical structure,
+  then canonical structure equations are used for the matching.
+\item If the head of \textit{term} is \emph{not} a constant, the
+  subterm should have the same structure ($\lambda$ abstraction,
+  \ssrC{let}$\dots$\ssrC{in} structure \dots).
+\item If the head of \textit{term} is a hole, the subterm should have
+  at least as many arguments as  \textit{term}. For instance the tactic:
+\begin{lstlisting}
+  set t := _ x.
+\end{lstlisting}
+transforms the goal \ssrL-x + y = z- into \ssrC{t y = z} and adds
+\ssrC{t := plus x : nat -> nat} to the context.
+
+\item In the special case where \textit{term} is of the form
+  \ssrC{(let f := }$t_0$ \ssrC{in f) }$t_1\dots t_n$,
+ then the pattern \textit{term} is treated
+as \ssrC{(_ }$t_1\dots t_n$\ssrC{)}. For each subterm in
+the goal having the form $(A\  u_1\dots u_{n'})$ with $n' \geq n$, the
+matching algorithm successively tries to find the largest
+partial application $(A\ u_1\dots u_{i'})$ convertible to the head
+$t_0$ of \textit{term}. For instance the following tactic:
+\begin{lstlisting}
+  set t := (let g y z := y.+1 + z in g) 2.
+\end{lstlisting}
+transforms the goal
+\begin{lstlisting}
+  (let f x y z := x + y + z in f 1) 2 3 = 6.
+\end{lstlisting}
+into \ssrC{t 3 = 6} and adds the local definition of \ssrC{t} to the
+context.
+\end{itemize}
+
+Moreover:
+\begin{itemize}
+\item Multiple holes in \textit{term} are treated as independent
+  placeholders. For instance, the tactic:
+\begin{lstlisting}
+  set t := _ + _.
+\end{lstlisting}
+transforms the goal \ssrC{x + y = z} into \ssrC{t = z} and pushes
+\ssrC{t := x + y : nat} in the context.
+\item The type of the subterm matched should fit the type
+  (possibly casted by some type annotations) of the pattern
+  \textit{term}.
+\item The replacement of the subterm found by the instantiated pattern
+  should not capture variables, hence the following script:
+\begin{lstlisting}
+  Goal forall x : nat, x + 1 = 0.
+  set u := _ + 1.
+\end{lstlisting}
+raises an error message, since \ssrC{x} is bound in the goal.
+\item Typeclass inference should fill in any residual hole, but
+matching should never assign a value to a global existential variable.
+
+\end{itemize}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Occurrence selection}\label{sssec:occselect}
+
+\ssr{} provides a generic syntax for the selection of occurrences by
+their position indexes. These \emph{occurrence switches} are shared by
+all
+\ssr{} tactics which require control on subterm selection like rewriting,
+generalization, \dots
+
+An \emph{occurrence switch} can be:
+\begin{itemize}
+\item A list \ssrC{\{} {\naturalnumber}$^*$ \ssrC{\}} of occurrences affected by the
+  tactic.
+For instance, the tactic:
+\begin{lstlisting}
+  set x := {1 3}(f 2).
+\end{lstlisting}
+transforms the goal \ssrC{f 2 + f 8 = f 2 + f 2} into
+\ssrC{x + f 8 = f 2  + x}, and adds the abbreviation
+\ssrC{x := f 2} in the
+context. Notice that some occurrences of a
+given term may be hidden to the user, for example because of a
+notation. The vernacular \ssrC{$\texttt{\textcolor{dkviolet}{Set }}$
+  Printing All} command displays all
+these hidden occurrences and should be used to find the correct
+coding of the occurrences to be selected\footnote{Unfortunately,
+even after a call to the Set Printing All command, some occurrences are
+still not displayed to the user, essentially the ones possibly hidden
+in the predicate of a dependent match structure.}. For instance, the
+following script:
+\begin{lstlisting}
+  Notation "a < b":= (le (S a) b).
+  Goal forall x y, x < y -> S x < S y.
+  intros x y; set t := S x.
+\end{lstlisting}
+generates the goal
+\ssrC{t <= y -> t < S y} since \ssrC{x < y} is now a notation for
+\ssrC{S x <= y}.
+\item A list \ssrC{\{}{\naturalnumber}$^+$\ssrC{\}}. This is equivalent to
+  \ssrC{\{} {\naturalnumber}$^+$ \ssrC{\}} but the list should start with a number, and
+  not with an Ltac variable.
+\item A list \ssrC{\{}{\naturalnumber}$^*$\ssrC{\}} of occurrences \emph{not} to be
+  affected by the tactic. For instance, the tactic:
+\begin{lstlisting}
+  set x := {-2}(f 2).
+\end{lstlisting}
+behaves like
+\begin{lstlisting}
+  set x := {1 3}(f 2).
+\end{lstlisting}
+on the goal \ssrL-f 2 + f 8 = f 2 + f 2- which has three occurrences of
+the the term \ssrC{f 2}
+\item In particular, the switch \ssrC{\{+\}} selects \emph{all} the
+  occurrences. This switch is useful to turn
+  off the default behavior of a tactic which automatically clears
+  some assumptions (see section \ref{ssec:discharge} for instance).
+\item The switch \ssrC{\{-\}} imposes that \emph{no} occurrences of the
+  term should be affected by the tactic. The tactic:
+\begin{lstlisting}
+  set x := {-}(f 2).
+\end{lstlisting}
+leaves the goal unchanged and adds the definition \ssrC{x := f 2} to the
+context. This kind of tactic may be used to take advantage of the
+power of the matching algorithm in a local definition, instead of
+copying large terms by hand.
+\end{itemize}
+
+
+It is important to remember that matching \emph{precedes} occurrence
+selection, hence the tactic:
+\begin{lstlisting}
+  set a := {2}(_ + _).
+\end{lstlisting}
+transforms the goal \ssrC{x + y = x + y + z} into \ssrC{x + y = a + z}
+and fails on the goal \\
+\ssrC{(x + y) + (z + z) = z + z} with the error message:
+\begin{lstlisting}
+  User error: only 1 < 2 occurrence of (x + y + (z + z))
+\end{lstlisting}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Localization}\label{ssec:loc}
+
+
+It is possible to define an abbreviation for a term appearing in the
+context of a goal thanks to the \ssrC{in} tactical.
+
+A tactic of the form:
+
+\begin{center}
+  \ssrC{set x :=} {\term} \ssrC{in} \ssrN[1]{fact}\ssrC{...}\ssrN[n]{fact}.
+\end{center}
+
+introduces a defined constant called \ssrC{x} in the context, and folds
+it in the facts \textit{fact$_1 \dots$ fact$_n$}
+The body of \ssrC{x} is the first subterm matching \textit{term} in
+\textit{fact$_1 \dots$ fact$_n$}.
+
+A tactic of the form:
+
+\begin{center}
+  \ssrC{set x :=} {\term} \ssrC{in} \ssrN[1]{fact}\ssrC{...}\ssrN[n]{fact} \ssrC{*.}
+\end{center}
+
+matches {\term} and then folds \ssrC{x} similarly in
+\textit{fact$_1 \dots$ fact$_n$}, but also folds \ssrC{x} in the goal.
+
+A goal \ssrL-x + t = 4-, whose context contains \ssrC{Hx : x = 3}, is left
+unchanged by the tactic:
+\begin{lstlisting}
+  set z := 3 in Hx.
+\end{lstlisting}
+but the context is extended with the definition \ssrC{z := 3} and \ssrC{Hx} becomes
+\ssrC{Hx : x = z}.
+On the same goal and context, the tactic:
+\begin{lstlisting}
+  set z := 3 in Hx *.
+\end{lstlisting}
+will moreover change the goal into \ssrL-x + t = S z-. Indeed, remember
+that \ssrC{4} is just a notation for \ssrC{(S 3)}.
+
+The use of the \ssrC{in} tactical is not limited to the localization of
+abbreviations: for a complete description of the \ssrC{in} tactical, see
+section \ref{ssec:profstack}.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Basic tactics}\label{sec:book}
+
+
+
+A sizable fraction of proof scripts consists of steps that do not
+"prove" anything new, but instead perform menial bookkeeping tasks
+such as selecting the names of constants and assumptions or splitting
+conjuncts. Although they are logically trivial, bookkeeping steps are
+extremely important because they define the structure of the data-flow
+of a proof script. This is especially true for reflection-based
+proofs, which often involve large numbers of constants and
+assumptions.  Good bookkeeping consists in always explicitly declaring
+(i.e., naming) all new constants and assumptions in the script, and
+systematically pruning irrelevant constants and assumptions in the
+context. This is essential in the context of an interactive
+development environment (IDE), because it facilitates navigating the
+proof, allowing to instantly "jump back" to the point at which a
+questionable assumption was added, and to find relevant assumptions by
+browsing the pruned context.  While novice or casual \Coq{} users may
+find the automatic name selection feature convenient, the usage of
+such a feature severely undermines the readability and maintainability
+of proof scripts, much like automatic variable declaration in programming
+languages. The \ssr{} tactics are therefore designed to support
+precise bookkeeping and to eliminate name generation heuristics.
+The bookkeeping features of \ssr{} are implemented as tacticals (or
+pseudo-tacticals), shared across most \ssr{} tactics, and thus form
+the foundation of the \ssr{} proof language.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Bookkeeping}\label{ssec:profstack}
+\idx{move: \dots{}}
+\idx{move=> \dots{}}
+\idx{move: \dots{} => \dots{}}
+\idx{\dots{} in \dots{}}
+
+During the course of a proof \Coq{} always present the user with
+a \emph{sequent} whose general form is
+\begin{displaymath}\begin{array}{l}
+%\arrayrulecolor{dkviolet}
+c_i\ \ssrC{:}\ T_i \\
+\dots\\
+d_j\ \ssrC{:=}\ e_j\ \ssrC{:}\ T_j \\
+\dots\\
+F_k\ \ssrC{:}\ P_k \\
+\dots \\[3pt]
+\hline\hline\\[-8pt]
+\ssrC{forall}\ \ssrC{(}x_\ell\ \ssrC{:}\ T_\ell\ssrC{)}\ \dots,\\
+\ssrC{let}\ y_m\ \ssrC{:=}\ b_m\ \ssrC{in}\ \dots\ \ssrC{in}\\
+P_n\ \ssrC{->}\ \dots\ \ssrC{->}\ C
+\end{array}\end{displaymath}
+The \emph{goal} to be proved appears below the double line; above the line is
+the \emph{context} of the sequent, a set of declarations of
+\emph{constants}~$c_i$, \emph{defined constants}~$d_i$, and
+\emph{facts}~$F_k$ that can be used to prove the goal (usually, $T_i,
+T_j\;:\;\ssrC{Type}$ and $P_k\;:\;\ssrC{Prop}$). The various kinds of
+declarations can come in any order. The top part of the context
+consists of declarations produced by the \ssrC{Section} commands
+\ssrC{Variable}, \ssrC{Let}, and \ssrC{Hypothesis}. This \emph{section context}
+is never affected by the \ssr{} tactics: they only operate on
+the lower part --- the \emph{proof context}.
+As in the figure above, the goal often decomposes into a series of
+(universally) quantified \emph{variables}
+$\ssrC{(}x_\ell\;\ssrC{:}\;T_\ell\ssrC{)}$, local \emph{definitions}
+$\ssrC{let}\;y_m\:\ssrC{:=}\;b_m\;\ssrC{in}$, and \emph{assumptions}
+$P_n\;\ssrC{->}$, and a \emph{conclusion}~$C$ (as in the context, variables,
+definitions, and assumptions can appear in any order). The conclusion
+is what actually needs to be proved --- the rest of the goal can be
+seen as a part of the proof context that happens to be ``below the line''.
+
+However, although they are logically equivalent, there are fundamental
+differences between constants and facts on the one hand, and variables
+and assumptions on the others. Constants and facts are
+\emph{unordered}, but \emph{named} explicitly in the proof text;
+variables and assumptions are \emph{ordered}, but \emph{unnamed}: the
+display names of variables may change at any time because of
+$\alpha$-conversion.
+
+Similarly, basic deductive steps such as \ssrC{apply} can only operate on
+the goal because the Gallina terms that control their action (e.g.,
+the type of the lemma used by \ssrC{apply}) only provide unnamed bound
+variables.\footnote{Thus scripts that depend on bound variable names, e.g.,
+via \ssrC{intros} or \ssrC{with}, are inherently fragile.}  Since the proof
+script can only refer directly to the context, it must constantly
+shift declarations from the goal to the context and conversely in
+between deductive steps.
+
+In \ssr{} these moves are performed by two \emph{tacticals} `\ssrC{=>}'
+and `\ssrC{:}', so that the bookkeeping required by a deductive step can
+be directly associated to that step, and that tactics in an \ssr{}
+script correspond to actual logical steps in the proof rather than
+merely shuffle facts. Still, some isolated bookkeeping is unavoidable,
+such as naming variables and assumptions at the beginning of a proof.
+\ssr{} provides a specific \ssrC{move} tactic for this purpose.
+
+Now \ssrC{move} does essentially nothing: it is mostly a placeholder for
+`\ssrC{=>}' and `\ssrC{:}'. The `\ssrC{=>}' tactical moves variables, local
+definitions, and assumptions to the context, while the `\ssrC{:}'
+tactical moves facts and constants to the goal. For example, the proof
+of\footnote{The name \ssrC{subnK} reads as
+``right cancellation rule for \ssrC{nat} subtraction''.}
+\begin{lstlisting}
+  Lemma |*subnK*| : forall m n, n <= m -> m - n + n = m.
+\end{lstlisting}\noindent
+might start with
+\begin{lstlisting}
+  move=> m n le_n_m.
+\end{lstlisting}
+where \ssrC{move} does nothing, but \ssrL|=> m n le_m_n| changes the
+variables and assumption of the goal in the constants \ssrC{m n : nat}
+and the fact \ssrL|le_n_m : n <= m|, thus exposing the conclusion\\
+ \ssrC{m - n + n = m}. 
+
+The `\ssrC{:}' tactical is the converse of `\ssrC{=>}': it removes facts
+and constants from the context by turning them into variables and assumptions.
+Thus
+\begin{lstlisting}
+  move: m le_n_m.
+\end{lstlisting}
+turns back \ssrC{m} and \ssrL|le_m_n| into a variable and an assumption, removing
+them from the proof context, and changing the goal to
+\begin{lstlisting}
+  forall m, n <= m -> m - n + n = m.
+\end{lstlisting}
+which can be proved by induction on \ssrC{n} using \ssrC{elim: n}.
+
+\noindent
+Because they are tacticals, `\ssrC{:}' and `\ssrC{=>}' can be combined, as in
+\begin{lstlisting}
+  move: m le_n_m => p le_n_p.
+\end{lstlisting}
+simultaneously renames \ssrL|m| and \ssrL|le_m_n| into \ssrL|p| and \ssrL|le_n_p|,
+respectively, by first turning them into unnamed variables, then
+turning these variables back into constants and facts.
+
+Furthermore, \ssr{} redefines the basic \Coq{} tactics \ssrC{case},
+\ssrC{elim}, and \ssrC{apply} so that they can take better advantage of
+'\ssrC{:}' and `\ssrC{=>}'. In there \ssr{} variants, these tactic operate
+on the first  variable or constant of the goal and they do not use or
+change the proof context. The `\ssrC{:}' tactical is used to operate on
+an element in the context. For instance the proof of \ssrC{subnK} could
+continue with
+\begin{lstlisting}
+  elim: n.
+\end{lstlisting}
+instead of \ssrC{elim n}; this has the advantage of
+removing \ssrC{n} from the context. Better yet, this \ssrC{elim} can be combined
+with previous \ssrC{move} and with the branching version of the \ssrC{=>} tactical
+(described in~\ref{ssec:intro}),
+to encapsulate the inductive step in a single command:
+\begin{lstlisting}
+  elim: n m le_n_m => [|n IHn] m => [_ | lt_n_m].
+\end{lstlisting}
+which breaks down the proof into two subgoals,
+\begin{lstlisting}
+  m - 0 + 0 = m
+\end{lstlisting}
+given \ssrC{m : nat}, and
+\begin{lstlisting}
+  m - S n + S n = m
+\end{lstlisting}
+given \ssrC{m n : nat}, \ssrL|lt_n_m : S n <= m|, and
+\begin{lstlisting}
+  IHn : forall m, n <= m -> m - n + n = m.
+\end{lstlisting}
+The '\ssrC{:}' and `\ssrC{=>}' tacticals can be explained very simply
+if one views the goal as a stack of variables and assumptions piled
+on a conclusion:
+\begin{itemize}
+\item {\tac} \ssrC{:} $a$ $b$ $c$ pushes the context constants $a$, $b$, $c$
+as goal variables \emph{before} performing {\tac}.
+\item {\tac} \ssrC{=>} $a$ $b$ $c$ pops the top three goal variables as
+context constants $a$, $b$, $c$, \emph{after} {\tac}
+has been performed.
+\end{itemize}
+These pushes and pops do not need to balance out as in the examples above,
+so
+\begin{lstlisting}
+  move: m le_n_m => p.
+\end{lstlisting}
+would rename \ssrC{m} into \ssrC{p}, but leave an extra assumption \ssrC{n <= p}
+in the goal.
+
+Basic tactics like \ssrC{apply} and \ssrC{elim} can also be used without the
+'\ssrC{:}' tactical: for example we can directly start a proof of \ssrC{subnK}
+by induction on the top variable \ssrC{m} with
+\begin{lstlisting}
+  elim=> [|m IHm] n le_n.
+\end{lstlisting}
+
+\noindent
+The general form of the localization tactical \ssrC{in} is also best
+explained in terms of the goal stack:
+
+\begin{center}
+  {\tac} \ssrC{in a H1 H2 *.}
+\end{center}
+
+is basically equivalent to
+
+\begin{center}
+  \ssrC{move: a H1 H2;} {\tac} \ssrC{=> a H1 H2.}
+\end{center}
+
+with two differences: the \ssrC{in} tactical will preserve the body of \ssrC{a} if
+\ssrC{a} is a defined constant, and if the `\ssrC{*}' is omitted it
+will use a temporary abbreviation to hide the statement of the goal
+from \ssrC{/*tactic*/}.
+
+The general form of the \ssrC{in} tactical can be used directly with
+the \ssrC{move}, \ssrC{case} and \ssrC{elim} tactics, so that one can write
+\begin{lstlisting}
+  elim: n => [|n IHn] in m le_n_m *.
+\end{lstlisting}
+instead of
+\begin{lstlisting}
+  elim: n m le_n_m => [|n IHn] m le_n_m.
+\end{lstlisting}
+This is quite useful for inductive proofs that involve many facts.
+
+\noindent See section \ref{ssec:gloc} for the general syntax and presentation
+of the \ssrC{in} tactical.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{The defective tactics}\label{ssec:basictac}
+
+In this section we briefly present the three basic tactics performing
+context manipulations and the main backward chaining tool.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{move} tactic.}\label{sssec:move}
+\idx{move}
+
+The \ssrC{move} tactic, in its
+defective form, behaves like the primitive \ssrC{hnf} \Coq{} tactic. For
+example, such a defective:
+\begin{lstlisting}
+  move.
+\end{lstlisting}
+exposes the first assumption in the goal, i.e. its changes the goal
+\ssrC{\~ False} into \ssrC{False -> False}.
+
+More precisely, the \ssrC{move} tactic inspects the goal and does nothing
+(\ssrC{idtac}) if an introduction step is possible, i.e. if the
+goal is a product or a \ssrC{let}$\dots$\ssrC{in}, and performs \ssrC{hnf}
+otherwise.
+
+Of course this tactic is most often used in combination with the
+bookkeeping tacticals (see section \ref{ssec:intro} and
+\ref{ssec:discharge}). These combinations mostly subsume the \ssrC{intros},
+\ssrC{generalize}, \ssrC{revert}, \ssrC{rename}, \ssrC{clear} and
+\textcolor{dkblue}{\texttt{pattern}} tactics.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{case} tactic.}
+\idx{case: \dots{}}
+
+The \ssrC{case} tactic performs
+\emph{primitive case analysis} on (co)inductive types; specifically,
+it destructs the top variable or assumption of the goal,
+exposing its constructor(s) and its arguments, as well as setting the value
+of its type family indices if it belongs to a type family
+(see section \ref{ssec:typefam}).
+
+The \ssr{} \ssrC{case} tactic has a special behavior on
+equalities.
+If the top assumption of the goal is an equality, the \ssrC{case} tactic
+``destructs'' it as a set of equalities between the constructor
+arguments of its left and right hand sides, as per the
+tactic \ssrC{injection}.
+For example, \ssrC{case} changes the goal
+\begin{lstlisting}
+  (x, y) = (1, 2) -> G.
+\end{lstlisting}
+into
+\begin{lstlisting}
+  x = 1 -> y = 2 -> G.
+\end{lstlisting}
+
+Note also that the case of \ssr{} performs \ssrC{False}
+elimination, even if no branch is generated by this case operation.
+Hence the command:
+\begin{lstlisting}
+  case.
+\end{lstlisting}
+on a goal of the form \ssrC{False -> G} will succeed and prove the goal.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{elim} tactic.} 
+\idx{elim: \dots{}}
+
+The \ssrC{elim} tactic performs
+inductive elimination on inductive types.
+The defective:
+\begin{lstlisting}
+  elim.
+\end{lstlisting}
+tactic performs inductive elimination on a goal whose top assumption
+has an inductive type. For example on goal of the form:
+\begin{lstlisting}
+  forall n : nat, m <= n
+\end{lstlisting}
+ in a context containing \ssrC{m : nat}, the
+\begin{lstlisting}
+  elim.
+\end{lstlisting}
+tactic produces two goals,
+\begin{lstlisting}
+  m <=  0
+\end{lstlisting}
+on one hand and
+\begin{lstlisting}
+  forall n : nat, m <= n -> m <= S n
+\end{lstlisting}
+on the other hand.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{apply} tactic.}\label{sssec:apply}
+\idx{apply: \dots{}}
+
+The \ssrC{apply} tactic is the main
+backward chaining tactic of the proof system. It takes as argument any
+\ssrC{/*term*/} and applies it to the goal.
+Assumptions in the type of \ssrC{/*term*/} that don't directly match the
+goal may generate one or more subgoals.
+
+In fact the \ssr{} tactic:
+\begin{lstlisting}
+  apply.
+\end{lstlisting}
+is a synonym for:
+\begin{lstlisting}
+  intro top; first [refine top | refine (top _) |  refine (top _ _) | ...]; clear top.
+\end{lstlisting}
+where \ssrC{top} is fresh name, and the sequence of \ssrC{refine} tactics
+tries to catch the appropriate number of wildcards to be inserted.
+Note that this use of the \ssrC{refine} tactic implies that the tactic
+tries to match the goal up to expansion of
+constants and evaluation of subterms.
+
+\ssr{}'s \ssrC{apply} has a special behaviour on goals containing
+existential metavariables of sort \ssrC{Prop}.  Consider the
+following example:
+\begin{lstlisting}
+Goal (forall y, 1 < y -> y < 2 -> exists x : { n | n < 3 }, proj1_sig x > 0).
+move=> y y_gt1 y_lt2; apply: (ex_intro _ (exist _ y _)).
+  by apply: gt_trans _ y_lt2.
+by move=> y_lt3; apply: lt_trans y_gt1.
+\end{lstlisting}
+Note that the last \ssrC{_} of the tactic \ssrC{apply: (ex_intro _ (exist _ y _))}
+represents a proof that \ssrC{y < 3}. Instead of generating the following
+goal
+\begin{lstlisting}
+   0 <  (n:=3) (m:=y) ?54
+\end{lstlisting}
+\noindent the system tries to prove \ssrC{y < 3} calling the \ssrC{trivial}
+tactic. If it succeeds, let's say because the context contains
+\ssrC{H : y < 3}, then the system generates the following goal:
+\begin{lstlisting}
+   0 < proj1_sig (exist (fun n => n < 3) y H
+\end{lstlisting}
+\noindent Otherwise the missing proof is considered to be irrelevant, and
+is thus discharged generating the following goals:
+\begin{lstlisting}
+   y < 3
+   forall H : y < 3, proj1_sig (exist (fun n => n < 3) y H)
+\end{lstlisting}
+Last, the user can replace the \ssrC{trivial} tactic by defining
+an Ltac expression named \ssrC{ssrautoprop}.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Discharge}\label{ssec:discharge}
+\idx{\dots{} : \dots{}}
+
+The general syntax of the discharging tactical `\ssrC{:}' is:
+\begin{center}
+	{\tac} \optional{\ssrN{ident}} \ssrC{:} \ssrN[1]{d-item} $\dots$ \ssrN[n]{d-item} \optional{\ssrN{clear-switch}}
+\end{center}
+where $n > 0$, and \ssrN{d-item} and \ssrN{clear-switch} are defined as
+\begin{longtable}{rcl}
+\ssrN{d-item} & ::= & \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} {\term} \\
+\ssrN{clear-switch}& ::=& \ssrC{\{} \ssrN[1]{ident}\, \ldots\,  \ssrN[m]{ident} \ssrC{\}}
+\end{longtable}
+with the following requirements:
+\begin{itemize}
+\item {\tac} must be one of the four basic tactics described
+      in~\ref{ssec:basictac}, i.e., \ssrC{move}, \ssrC{case}, \ssrC{elim} or \ssrC{apply},
+      the \ssrC{exact} tactic (section \ref{ssec:termin}),
+      the \ssrC{congr} tactic (section \ref{ssec:congr}), or the application
+      of the \emph{view} tactical `\ssrC{/}' (section \ref{ssec:assumpinterp})
+      to one of \ssrC{move}, \ssrC{case}, or \ssrC{elim}.
+\item The optional \ssrN{ident} specifies \emph{equation generation}
+      (section \ref{ssec:equations}), and is only allowed if {\tac}
+      is \ssrC{move}, \ssrC{case} or \ssrC{elim}, or the application of the
+      view tactical `\ssrC{/}' (section \ref{ssec:assumpinterp})
+      to \ssrC{case} or \ssrC{elim}.
+\item An \ssrN{occ-switch} selects occurrences of {\term},
+      as in \ref{sssec:occselect}; \ssrN{occ-switch} is not allowed if
+      {\tac} is \ssrC{apply} or \ssrC{exact}.
+\item A clear item \ssrN{clear-switch} specifies facts and constants to be
+  deleted from the proof context (as per the \ssrC{clear} tactic).
+\end{itemize}
+The `\ssrC{:}' tactical first \emph{discharges} all the \ssrN{d-item}s,
+right to left, and then performs {\tac}, i.e., for each \ssrN{d-item},
+starting with $\ssrN[n]{d-item}$:
+\begin{enumerate}
+\item The \ssr{} matching algorithm described in section~\ref{ssec:set}
+      is used to find occurrences of {\term} in the goal,
+      after filling any holes `\ssrC{_}' in {\term}; however if {\tac}
+      is \ssrC{apply} or \ssrC{exact} a different matching algorithm,
+      described below, is used
+      \footnote{Also, a slightly different variant may be used for the first
+      \ssrN{d-item} of \ssrC{case} and \ssrC{elim}; see section~\ref{ssec:typefam}.}.
+\item~\label{enum:gen} These occurrences are replaced by a new
+  variable; in particular,
+      if {\term} is a fact, this adds an assumption to the goal.
+\item~\label{enum:clr} If {\term} is \emph{exactly} the name of a constant
+      or fact in the proof context, it is deleted from the context,
+      unless there is an \ssrN{occ-switch}.
+\end{enumerate}
+Finally, {\tac} is performed just after $\ssrN[1]{d-item}$ has been
+generalized ---
+that is, between steps \ref{enum:gen} and \ref{enum:clr} for $\ssrN[1]{d-item}$.
+The names listed in the final \ssrN{clear-switch} (if it is present)
+are cleared first, before $\ssrN[n]{d-item}$ is discharged.
+
+\noindent
+Switches affect the discharging of a \ssrN{d-item} as follows:
+\begin{itemize}
+\item An \ssrN{occ-switch} restricts generalization (step~\ref{enum:gen})
+      to a specific subset of the occurrences of {\term}, as per
+      \ref{sssec:occselect}, and prevents clearing (step~\ref{enum:clr}).
+\item All the names specified by a \ssrN{clear-switch} are deleted from the
+      context in step~\ref{enum:clr}, possibly in addition to {\term}.
+\end{itemize}
+For example, the tactic:
+\begin{lstlisting}
+  move: n {2}n (refl_equal n).
+\end{lstlisting}
+\begin{itemize}
+\item first generalizes \ssrC{(refl_equal n : n = n)};
+\item then generalizes the second occurrence of \ssrC{n}.
+\item finally generalizes all the other occurrences of \ssrC{n},
+      and clears \ssrC{n} from the proof context
+      (assuming \ssrC{n} is a proof constant).
+\end{itemize}
+Therefore this tactic changes any goal \ssrC{G} into
+\begin{lstlisting}
+ forall n n0 : nat, n = n0 -> G.
+\end{lstlisting}
+where the name \ssrC{n0} is picked by the \Coq{} display function,
+and assuming \ssrC{n} appeared only in~\ssrC{G}.
+
+Finally, note that a discharge operation generalizes defined constants
+as variables, and not as local definitions. To override this behavior,
+prefix the name of the local definition with a \ssrC{@},
+like in \ssrC{move: @n}.
+
+This is in contrast with the behavior of the \ssrC{in} tactical (see section
+\ref{ssec:gloc}), which preserves local definitions by default.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Clear rules}
+
+The clear step will fail if {\term} is a proof constant that
+appears in other facts; in that case either the facts should be
+cleared explicitly with a \ssrN{clear-switch}, or the clear step should be
+disabled. The latter can be done by adding an \ssrN{occ-switch} or simply by
+putting parentheses around {\term}: both
+\begin{lstlisting}
+  move: (n).
+\end{lstlisting}
+and
+\begin{lstlisting}
+  move: {+}n.
+\end{lstlisting}
+generalize \ssrC{n} without clearing \ssrC{n} from the proof context.
+
+The clear step will also fail if the \ssrN{clear-switch} contains a
+\ssrN{ident} that is not in the \emph{proof} context.
+Note that \ssr{} never clears a section constant.
+
+If {\tac} is \ssrC{move} or \ssrC{case} and an equation \ssrN{ident} is given,
+then clear (step~\ref{enum:clr}) for $\ssrN[1]{d-item}$ is suppressed
+(see section \ref{ssec:equations}).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Matching for \ssrC{apply} and \ssrC{exact}}\label{sss:strongapply}
+
+The matching algorithm for \ssrN{d-item}s of the \ssr{} \ssrC{apply} and
+\ssrC{exact} tactics
+exploits the type of $\ssrN[1]{d-item}$ to interpret
+wildcards in the other \ssrN{d-item} and to determine which occurrences of
+these should be generalized.
+Therefore, \ssrN{occur switch}es are not needed for \ssrC{apply} and \ssrC{exact}.
+
+Indeed, the \ssr{} tactic \ssrC{apply: H x} is equivalent to
+\begin{lstlisting}
+  refine (@H _ ... _ x); clear H x
+\end{lstlisting}
+with an appropriate number of wildcards between \ssrC{H} and~\ssrC{x}.
+
+Note that this means that matching for \ssrC{apply} and \ssrC{exact} has
+much more context to interpret wildcards; in particular it can accommodate
+the `\ssrC{_}' \ssrN{d-item}, which would always be rejected after `\ssrC{move:}'.
+For example, the tactic
+\begin{lstlisting}
+  apply: trans_equal (Hfg _) _.
+\end{lstlisting}
+transforms the goal \ssrC{f a = g b}, whose context contains
+\ssrC{(Hfg : forall x, f x = g x)}, into \ssrC{g a = g b}.
+This tactic is equivalent (see section \ref{ssec:profstack}) to:
+\begin{lstlisting}
+  refine (trans_equal (Hfg _) _).
+\end{lstlisting}
+and this is a common idiom for applying transitivity on the left hand side
+of an equation.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{abstract} tactic}\label{ssec:abstract}
+\idx{abstract: \dots{}}
+
+The \ssrC{abstract} tactic assigns an abstract constant previously introduced with
+the \ssrC{[: name ]} intro pattern (see section~\ref{ssec:intro},
+page~\pageref{ssec:introabstract}).
+In a goal like the following:
+\begin{lstlisting}
+ m : nat
+ abs : <hidden>
+ n : nat
+ =============
+ m < 5 + n
+\end{lstlisting}
+The tactic \ssrC{abstract: abs n} first generalizes the goal with respect to
+\ssrC{n} (that is not visible to the abstract constant \ssrC{abs}) and then
+assigns \ssrC{abs}.  The resulting goal is:
+\begin{lstlisting}
+ m : nat
+ n : nat
+ =============
+ m < 5 + n
+\end{lstlisting}
+Once this subgoal is closed, all other goals having \ssrC{abs} in their context
+see the type assigned to \ssrC{abs}.  In this case:
+\begin{lstlisting}
+ m : nat
+ abs : forall n, m < 5 + n
+\end{lstlisting}
+
+For a more detailed example the user should refer to section~\ref{sssec:have},
+page~\pageref{sec:havetransparent}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Introduction}\label{ssec:intro}
+\idx{\dots{} => \dots{}}
+
+The application of a tactic to a given goal can generate
+(quantified) variables, assumptions, or definitions, which the user may want to
+\emph{introduce} as new facts, constants or defined constants, respectively.
+If the tactic splits the goal into several subgoals,
+each of them may require the introduction of different constants and facts.
+Furthermore it is very common to immediately decompose
+or rewrite with an assumption instead of adding it to the context,
+as the goal can often be simplified and even
+proved after this.
+
+All these operations are performed by the introduction tactical
+`\ssrC{=>}', whose general syntax is
+\begin{center}
+	{\tac} \ssrC{=>} \ssrN[1]{i-item} $\dots$ \ssrN[n]{i-item}
+\end{center}
+where {\tac} can be any tactic, $n > 0$ and
+\begin{longtable}{rcl}
+  \ssrN{i-item}& ::=& \ssrN{i-pattern} {\optsep} \ssrN{s-item} {\optsep} \ssrN{clear-switch} {\optsep} \ssrC{/}{\term} \\
+  \ssrN{s-item}& ::=& \ssrC{/=} {\optsep} \ssrC{//} {\optsep} \ssrC{//=} \\
+  \ssrN{i-pattern}& ::=& \ssrN{ident} {\optsep} \ssrC{_} {\optsep} \ssrC{?} {\optsep} \ssrC{*} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{->} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{<-} {\optsep} \\
+	   &&      \ssrC{[} \ssrN[1]{i-item}$^*$ \ssrC{|} $\dots$ \ssrC{|} \ssrN[m]{i-item}$^*$ \ssrC{]} {\optsep} \ssrC{-} {\optsep} \ssrC{[:} \ssrN{ident}$^+$ \ssrC{]}
+\end{longtable}
+
+The `\ssrC{=>}' tactical first executes {\tac}, then the
+\ssrN{i-item}s, left to right, i.e., starting from $\ssrN[1]{i-item}$.  An
+\ssrN{s-item} specifies a simplification operation; a $\ssrN{clear
+switch}$ specifies context pruning as in~\ref{ssec:discharge}. The
+\ssrN{i-pattern}s can be seen as a variant of \emph{intro patterns}~\ref{intros-pattern}:
+each performs an introduction operation, i.e., pops some variables or
+assumptions from the goal.
+
+An \ssrN{s-item} can simplify the set of subgoals or the subgoal themselves:
+\begin{itemize}
+\item \ssrC{//} removes all the ``trivial'' subgoals that can be resolved by
+      the \ssr{} tactic \ssrC{done} described in~\ref{ssec:termin}, i.e., it
+      executes \ssrC{try done}.
+\item \ssrC{/=} simplifies the goal by performing partial evaluation, as
+   per the tactic \ssrC{simpl}.\footnote{Except \ssrC{/=} does not
+   expand the local definitions created by the \ssr{} \ssrC{in} tactical.}
+\item \ssrC{//=} combines both kinds of simplification; it is equivalent
+    to \ssrC{/= //}, i.e., \ssrC{simpl; try done}.
+\end{itemize}
+When an \ssrN{s-item} bears a \ssrN{clear-switch}, then the \ssrN{clear-switch} is
+executed \emph{after} the \ssrN{s-item}, e.g., \ssrL|{IHn}//| will solve
+some subgoals, possibly using the fact \ssrL|IHn|, and will erase \ssrL|IHn|
+from the context of the remaining subgoals.
+
+The last entry in the \ssrN{i-item} grammar rule, \ssrC{/}{\term},
+represents a view (see section~\ref{sec:views}). If $\ssrN[k+1]{i-item}$
+is a view \ssrN{i-item}, the view is applied to the assumption in top
+position once $\ssrN[1]{i-item} \dots \ssrN[k]{i-item}$ have been performed.
+
+The view is applied to the top assumption.
+
+\ssr{} supports the following \ssrN{i-pattern}s:
+\begin{itemize}
+\item \ssrN{ident} pops the top variable, assumption, or local definition into
+      a new constant, fact, or defined constant \ssrN{ident}, respectively.
+      Note that defined constants cannot be introduced when
+      $\delta$-expansion is required to expose the top variable or assumption.
+\item \ssrC{?} pops the top variable into an anonymous constant or fact,
+      whose name is picked by the tactic interpreter.
+      \ssr{} only generates names that
+      cannot appear later in the user script.\footnote{\ssr{} reserves
+      all identifiers of the form ``\ssrC{_x_}'', which is used for such
+      generated names.}
+\item \ssrC{_} pops the top variable into an anonymous constant that will be
+     deleted from
+     the proof context of all the subgoals produced by the \ssrC{=>} tactical.
+     They should thus never be displayed, except in an error message
+     if the constant is still actually used in the goal or context after
+     the last \ssrN{i-item} has been executed (\ssrN{s-item}s can erase goals
+     or terms where the constant appears).
+\item \ssrC{*} pops all the remaining apparent variables/assumptions
+     as anonymous constants/facts. Unlike \ssrC{?} and \ssrC{move} the \ssrC{*}
+     \ssrN{i-item} does not expand definitions in the goal to expose
+     quantifiers, so it may be useful to repeat a \ssrC{move=> *} tactic,
+     e.g., on the goal
+\begin{lstlisting}
+  forall a b : bool, a <> b
+\end{lstlisting}
+a first \ssrC{move=> *} adds only \ssrC{_a_ : bool} and \ssrC{_b_ : bool} to
+the context; it takes a second \ssrC{move=> *} to add
+\ssrC{_Hyp_ : _a_ = _b_}.
+\item $[\ssrN{occ-switch}]$\ssrC{->} (resp. $[\ssrN{occ-switch}]$\ssrC{<-})
+  pops the top assumption
+  (which should be a rewritable proposition) into an anonymous fact,
+  rewrites (resp. rewrites right to left) the goal with this fact
+  (using the \ssr{} \ssrC{rewrite} tactic described in section~\ref{sec:rw},
+  and honoring the optional occurrence selector),
+  and finally deletes the anonymous fact from the context.
+\item\ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]},
+   when it is the very \emph{first} \ssrN{i-pattern} after ${\tac}\;\ssrC{=>}$
+   tactical \emph{and} {\tac} is not a \ssrC{move}, is a \emph{branching}
+   \ssrN{i-pattern}. It executes
+   the sequence $\ssrN[i]{i-item}^*$ on the $i^{\rm th}$
+   subgoal produced by {\tac}. The execution of {\tac}
+   should thus generate exactly $m$
+   subgoals, unless the \ssrC{[$\dots$]} \ssrN{i-pattern} comes after an initial
+   \ssrC{//} or \ssrC{//=} \ssrN{s-item} that closes some of the goals produced by
+   {\tac}, in which case exactly $m$ subgoals should remain after the
+   \ssrN{s-item}, or we have the trivial branching \ssrN{i-pattern} \ssrC{[]},
+   which always does nothing, regardless of the number of remaining subgoals.
+\item\ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]}, when it is
+   \emph{not} the first \ssrN{i-pattern} or when {\tac} is a
+   \ssrC{move}, is a \emph{destructing} \ssrN{i-pattern}.  It starts by
+   destructing the top variable, using the \ssr{} \ssrC{case} tactic
+   described in~\ref{ssec:basictac}.  It then behaves as the
+   corresponding branching \ssrN{i-pattern}, executing the sequence
+   $\ssrN[i]{i-item}^*$ in the $i^{\rm th}$ subgoal generated by the case
+   analysis; unless we have the trivial destructing \ssrN{i-pattern}
+   \ssrC{[]}, the latter should generate exactly $m$ subgoals, i.e., the
+   top variable should have an inductive type with exactly $m$
+   constructors.\footnote{More precisely, it should have a quantified
+   inductive type with $a$ assumptions and $m - a$ constructors.}
+   While it is good style to use the $\ssrN[i]{i-item}^*$
+   to pop the variables and assumptions corresponding to each constructor,
+   this is not enforced by \ssr{}.
+\item\ssrC{-} does nothing, but counts as an intro pattern. It can also
+  be used to force the interpretation of
+  \ssrC{[ $\ssrN[1]{i-item}^*$ | $\dots$ | $\ssrN[m]{i-item}^*$ ]}
+   as a case analysis like in \ssrC{move=> -[H1 H2]}. It can also be used
+   to indicate explicitly the link between a view and a name like in
+   \ssrC{move=> /eqP-H1}. Last, it can serve as a separator between
+   views. Section~\ref{ssec:multiview} explains in which respect
+   the tactic \ssrC{move=> /v1/v2} differs from the tactic
+   \ssrC{move=> /v1-/v2}.
+\item\ssrC{[: $\ssrN{ident}^+$ ]} introduces in the context an abstract constant
+   for each \ssrN{ident}.  Its type has to be fixed later on by using
+   the \ssrC{abstract} tactic (see page~\pageref{ssec:abstract}).  Before then
+   the type displayed is \ssrC{<hidden>}.\label{ssec:introabstract}
+\end{itemize}
+Note that \ssr{} does not support the syntax
+$\ssrC{(}\ssrN{ipat}\ssrC{,}\dots\ssrC{,}\ssrN{ipat}\ssrC{)}$ for destructing
+intro-patterns.
+
+Clears are deferred until the end of the intro pattern. For
+example, given the goal:
+\begin{lstlisting}
+x, y : nat
+==================
+0 < x = true -> (0 < x) && (y < 2) = true
+\end{lstlisting}
+the tactic \ssrC{move=> \{x\} ->} successfully rewrites the goal and
+deletes \ssrC{x} and the anonymous equation. The goal is thus turned into:
+\begin{lstlisting}
+y : nat
+==================
+true && (y < 2) = true
+\end{lstlisting}
+If the cleared names are reused in the same intro pattern, a renaming
+is performed behind the scenes.
+
+Facts mentioned in a clear switch must be valid
+names in the proof context (excluding the section context).
+
+The rules for interpreting branching and destructing \ssrN{i-pattern}
+are motivated by the fact that it would be pointless to have a branching
+pattern if {\tac} is a \ssrC{move}, and in most of the remaining cases
+{\tac} is \ssrC{case} or \ssrC{elim}, which implies destruction.
+The rules above imply that
+\begin{lstlisting}
+  move=> [a b].
+  case=> [a b].
+  case=> a b.
+\end{lstlisting}
+are all equivalent, so which one to use is a matter of style;
+\ssrC{move} should be used for casual decomposition,
+such as splitting a pair, and \ssrC{case} should be used for actual decompositions,
+in particular for type families (see~\ref{ssec:typefam})
+and proof by contradiction.
+
+The trivial branching \ssrN{i-pattern} can be used to force the branching
+interpretation, e.g.,
+\begin{lstlisting}
+  case=> [] [a b] c.
+  move=> [[a b] c].
+  case;  case=> a b c.
+\end{lstlisting}
+are all equivalent.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Generation of equations}\label{ssec:equations}
+\idx{move eq : \dots{}}
+
+The generation of named equations option stores the definition of a
+new constant as an equation. The tactic:
+\begin{lstlisting}
+  move En: (size l) => n.
+\end{lstlisting}
+where \ssrC{l} is a list, replaces \ssrC{size l} by \ssrC{n} in the goal and
+adds the fact \ssrC{En : size l = n} to the context.
+ This is quite different from:
+\begin{lstlisting}
+  pose n := (size l).
+\end{lstlisting}
+which generates a definition \ssrC{n := (size l)}. It is not possible to
+generalize or
+rewrite such a definition; on the other hand, it is automatically
+expanded during
+computation, whereas expanding the equation \ssrC{En} requires explicit
+rewriting.
+
+The use of this equation name generation option with a \ssrC{case} or an
+\ssrC{elim} tactic changes the status of the first \iitem{}, in order to
+deal with the possible parameters of the constants introduced.
+
+On the
+goal \ssrC{a <> b} where \ssrC{a, b} are natural numbers, the tactic:
+\begin{lstlisting}
+  case E : a => [|n].
+\end{lstlisting}
+generates two subgoals. The equation \ssrC{E : a = 0}  (resp. \ssrC{E : a =
+  S n}, and the constant \ssrC{n : nat}) has been added to
+the context of the goal \ssrC{0 <> b} (resp. \ssrC{S n  <> b}).
+
+If the user does not provide a branching \iitem{} as first \iitem{},
+or if the \iitem{} does not provide enough names for the arguments of
+a constructor,
+then the constants generated are introduced under fresh \ssr{} names.
+For instance, on the goal \ssrC{a <> b}, the tactic:
+\begin{lstlisting}
+  case E : a => H.
+\end{lstlisting}
+also generates two subgoals, both requiring a proof of \ssrC{False}.
+ The hypotheses \ssrC{E : a = 0} and
+\ssrC{H : 0 = b} (resp. \ssrC{E : a = S _n_} and
+\ssrC{H : S _n_ = b}) have been added to the context of the first
+subgoal (resp. the second subgoal).
+
+Combining the generation of named equations mechanism with the
+\ssrC{case} tactic strengthens the power of a case analysis. On the other
+hand, when combined with the \ssrC{elim} tactic, this feature is mostly
+useful for
+debug purposes, to trace the values of decomposed parameters and
+pinpoint failing branches.
+
+% This feature is also useful
+% to analyse and debug generate-and-test style scripts that prove program
+% properties by generating a large set of input patterns and uniformly
+% solving the corresponding subgoals by computation and rewriting, e.g,
+
+% \begin{lstlisting}
+%   case: et => [|e' et]; first by case: s.
+%   case: e => //; case: b; case: w.
+% \end{lstlisting}
+% If the above sequence fails, then it's easy enough to replace the line
+% above with
+% \begin{lstlisting}
+%   case: et => [|e' et].
+%   case Ds: s; case De: e => //; case Db: b; case Dw: w=> [|s' w'] //=.
+% \end{lstlisting}
+% Then the first subgoal that appears will be the failing one, and the
+% equations \ssrC{Ds}, \ssrC{De}, \ssrC{Db}
+% and \ssrC{Dw} will pinpoint its branch. When the constructors of
+% the decomposed type have arguments (like \ssrC{w : (seq nat)}
+% above) these need to be
+% introduced in order to generate the equation, so there should
+% always be an explicit \iitem{} (\ssrC{\[|s' w'\]} above) that
+% assigns names to these arguments. If this \iitem{}
+% is omitted the arguments are introduced with default
+% name; this
+% feature should be
+% avoided except for quick debugging runs (it has some uses in complex tactic
+% sequences, however).
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Type families}\label{ssec:typefam}
+\idx{case: \dots{} / \dots{}}
+
+When the top assumption of a goal has an inductive type, two
+specific operations are possible: the case analysis performed by the
+\ssrC{case} tactic, and the application of an induction principle,
+performed by the \ssrC{elim} tactic. When this top assumption has an
+inductive type, which is moreover an instance of a type family, \Coq{}
+may need help from the user to specify which occurrences of the parameters
+of the type should be substituted.
+
+A specific \ssrC{/} switch indicates the type family parameters of the
+type of a \ditem{} immediately following this \ssrC{/} switch, using the
+syntax:
+
+\begin{center}
+ \ssrC{[} \ssrC{case} {\optsep} \ssrC{elim} \ssrC{]:} \ssrN{d-item}$^+$ \ssrC{/} \ssrN{d-item}$^*$
+\end{center}
+
+The \ssrN{d-item}s on the right side of the \ssrC{/} switch are discharged
+as described in section \ref{ssec:discharge}. The case analysis or
+elimination will be done on the type of the top assumption after these
+discharge operations.
+
+Every \ssrN{d-item} preceding the \ssrC{/} is interpreted as arguments of this
+type, which should be an instance of an inductive type family. These terms are
+not actually generalized, but rather selected for substitution. Occurrence
+switches can be used to restrict the substitution.  If a {\term} is left
+completely implicit (e.g. writing just $\ssrC{\_}$), then a pattern is inferred
+looking at the type of the top assumption.  This allows for the compact syntax
+\ssrC{case: \{2\}\_ / eqP}, were \ssrC{\_} is interpreted as \ssrC{(\_ == \_)}. Moreover
+if the \ssrN{d-item}s list is too short, it is padded with an initial
+sequence of $\ssrC{\_}$ of the right length.
+
+Here is a small example on lists. We define first a function which
+adds an element at the end of a given list.
+\begin{lstlisting}
+  Require Import List.
+
+  Section LastCases.
+  Variable A : Type.
+
+  Fixpoint |*add_last*|(a : A)(l : list A): list A :=
+  match l with
+    |nil => a :: nil
+    |hd :: tl => hd :: (add_last a tl)
+  end.
+\end{lstlisting}
+Then we define an inductive predicate for
+case analysis on lists according to their last element:
+\begin{lstlisting}
+  Inductive |*last_spec*| : list A -> Type :=
+    | LastSeq0 : last_spec nil
+    | LastAdd s x : last_spec (add_last x s).
+
+  Theorem |*lastP*| : forall l : list A, last_spec l.
+\end{lstlisting}
+Applied to the goal:
+\begin{lstlisting}
+  Goal forall l : list A, (length l) * 2 = length (app l l).
+\end{lstlisting}
+the command:
+\begin{lstlisting}
+  move=> l; case: (lastP l).
+\end{lstlisting}
+generates two subgoals:
+\begin{lstlisting}
+  length nil * 2 = length (nil ++ nil)
+\end{lstlisting}
+and
+\begin{lstlisting}
+  forall (s : list A) (x : A),
+    length (add_last x s) * 2 = length (add_last x s ++ add_last x s)
+\end{lstlisting}
+both having \ssrC{l : list A} in their context.
+
+Applied to the same goal, the command:
+\begin{lstlisting}
+  move=> l; case: l / (lastP l).
+\end{lstlisting}
+generates the same subgoals but \ssrC{l} has been cleared from both
+contexts.
+
+Again applied to the same goal, the command:
+\begin{lstlisting}
+  move=> l; case: {1 3}l / (lastP l).
+\end{lstlisting}
+generates the subgoals \ssrL-length l * 2 = length (nil ++ l)- and
+\ssrL-forall (s : list A) (x : A), length l * 2 = length (add_last x s++l)-
+where the selected occurrences on the left of the \ssrC{/} switch have
+been substituted with \ssrC{l} instead of being affected by the case
+analysis.
+
+The equation name generation feature combined with a type family \ssrC{/}
+  switch generates an equation for the \emph{first} dependent d-item
+specified by the user.
+Again starting with the above goal, the command:
+\begin{lstlisting}
+  move=> l; case E: {1 3}l / (lastP l)=>[|s x].
+\end{lstlisting}
+adds \ssrC{E : l = nil} and \ssrC{E : l = add_last x s},
+respectively, to the context of the two subgoals it generates.
+
+There must be at least one \emph{d-item} to the left of the \ssrC{/}
+switch; this prevents any
+confusion with the view feature. However, the \ditem{}s to the right of
+the \ssrC{/} are optional, and if they are omitted the first assumption
+provides the instance of the type family.
+
+The equation always refers to the first \emph{d-item} in the actual
+tactic call, before any padding with initial $\ssrC{\_}$s. Thus, if an
+inductive type has two family parameters, it is possible to have
+\ssr{} generate an equation for the second one by omitting the pattern
+for the first; note however that this will fail if the type of the
+second parameter depends on the value of the first parameter.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Control flow}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Indentation and bullets}\label{ssec:indent}
+
+A linear development of \Coq{} scripts gives little information on
+the structure of the proof. In addition, replaying a proof after some
+changes in the statement to be proved will usually not display information to
+distinguish between the various branches of case analysis for instance.
+
+To help the user in this organization of the proof script at
+development time, \ssr{} provides some bullets to highlight the
+structure of branching proofs. The available bullets are \ssrC{-},
+\ssrC{+} and \ssrC{*}. Combined with tabulation, this lets us highlight four
+nested levels of branching; the most we have ever
+needed is three. Indeed, the use of ``simpl and closing'' switches, of
+terminators (see above section \ref{ssec:termin}) and selectors (see
+ section \ref{ssec:select}) is powerful enough
+to avoid most of the time more than two levels of indentation.
+
+Here is a fragment of such a structured script:
+
+\begin{lstlisting}
+case E1: (abezoutn _ _) => [[| k1] [| k2]].
+- rewrite !muln0 !gexpn0 mulg1 => H1.
+  move/eqP: (sym_equal F0); rewrite -H1 orderg1 eqn_mul1.
+  by case/andP; move/eqP.
+- rewrite muln0 gexpn0 mulg1 => H1.
+  have F1: t %| t * S k2.+1 - 1.
+    apply: (@dvdn_trans (orderg x)); first by rewrite F0; exact: dvdn_mull.
+    rewrite orderg_dvd; apply/eqP; apply: (mulgI x).
+    rewrite -{1}(gexpn1 x) mulg1 gexpn_add leq_add_sub //.
+    by move: P1; case t.
+  rewrite dvdn_subr in F1; last by exact: dvdn_mulr.
+  + rewrite H1 F0 -{2}(muln1 (p ^ l)); congr (_ * _).
+    by apply/eqP; rewrite -dvdn1.
+  + by move: P1; case: (t) => [| [| s1]].
+- rewrite muln0  gexpn0 mul1g => H1.
+...
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Terminators}\label{ssec:termin}
+\idx{by \dots{}}
+
+To further structure scripts, \ssr{}
+supplies \emph{terminating} tacticals to explicitly close off tactics.
+When replaying scripts, we then have the nice property that
+an error immediately occurs when a closed tactic fails to prove its
+subgoal.
+
+It is hence recommended practice that the proof of any subgoal should
+end with a tactic which \emph{fails if it does not solve the current
+  goal}, like \ssrC{discriminate}, \ssrC{contradiction} or \ssrC{assumption}.
+
+In fact, \ssr{} provides a generic tactical which turns any tactic into
+a closing one (similar to \ssrC{now}). Its general syntax is:
+
+\begin{center}
+  \ssrC{by} {\tac}\ssrC{.}
+\end{center}
+
+The Ltac expression:
+
+\begin{center}
+  \ssrC{by [}\ssrN[1]{tactic} \ssrC{| [}\ssrN[2]{tactic} \ssrC{| ...].}
+\end{center}
+
+is equivalent to:
+
+\begin{center}
+  \ssrC{[by} \ssrN[1]{tactic} \ssrC{| by} \ssrN[2]{tactic} \ssrC{| ...].}
+\end{center}
+
+and this form should be preferred to the former.
+
+In the script provided as example in section \ref{ssec:indent}, the
+paragraph corresponding to each sub-case ends with a tactic line prefixed
+with a \ssrC{by}, like in:
+
+\begin{center}
+  \ssrC{by apply/eqP; rewrite -dvdn1.}
+\end{center}
+
+
+The \ssrC{by} tactical is implemented using the user-defined,
+and extensible \ssrC{done} tactic. This \ssrC{done} tactic tries to solve
+the current goal by some trivial means and fails if it doesn't succeed.
+Indeed, the tactic expression:
+
+\begin{center}
+   \ssrC{by} {\tac}\ssrC{.}
+\end{center}
+
+is equivalent to:
+
+\begin{center}
+  {\tac}\ssrC{; done.}
+\end{center}
+
+Conversely, the tactic
+
+\begin{center}
+  \ssrC{by [ ].}
+\end{center}
+
+is equivalent to:
+
+\begin{center}
+  \ssrC{done.}
+\end{center}
+
+The default implementation of the \ssrC{done} tactic, in the {\tt
+  ssreflect.v} file, is:
+
+\begin{lstlisting}
+Ltac done :=
+  trivial; hnf; intros; solve
+   [ do ![solve [trivial | apply: sym_equal; trivial]
+         | discriminate | contradiction | split]
+   | case not_locked_false_eq_true; assumption
+   | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
+\end{lstlisting}
+
+The lemma \ssrC{|*not_locked_false_eq_true*|} is needed to discriminate
+\emph{locked} boolean predicates (see section \ref{ssec:lock}).
+The iterator tactical \ssrC{do} is presented in section
+\ref{ssec:iter}.
+This tactic can be customized by the user, for instance to include an
+\ssrC{auto} tactic.
+
+A natural and common way of closing a goal is to apply a lemma which
+is the \ssrC{exact} one needed for the goal to be solved. The defective
+form of the tactic:
+\begin{lstlisting}
+  exact.
+\end{lstlisting}
+is equivalent to:
+\begin{lstlisting}
+  do [done | by move=> top; apply top].
+\end{lstlisting}
+where \ssrC{top} is a fresh name affected to the top assumption of the goal.
+This applied form is supported by the  \ssrC{:} discharge tactical, and
+the tactic:
+\begin{lstlisting}
+  exact: MyLemma.
+\end{lstlisting}
+is equivalent to:
+\begin{lstlisting}
+  by apply: MyLemma.
+\end{lstlisting}
+(see section \ref{sss:strongapply} for the documentation of the \ssrC{apply:}
+combination).
+
+\textit{Warning} The list of tactics, possibly chained by
+semi-columns, that follows a \ssrC{by} keyword is considered as a
+parenthesized block
+applied to the current goal. Hence for example if the tactic:
+\begin{lstlisting}
+   by rewrite my_lemma1.
+\end{lstlisting}
+succeeds, then the tactic:
+\begin{lstlisting}
+   by rewrite my_lemma1; apply my_lemma2.
+\end{lstlisting}
+usually fails since it is equivalent to:
+\begin{lstlisting}
+   by (rewrite my_lemma1; apply my_lemma2).
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Selectors}\label{ssec:select}
+\idx{last \dots{} first}
+\idx{first \dots{} last}
+
+When composing tactics, the two tacticals \ssrC{first} and
+\ssrC{last} let the user restrict the application of a tactic to only one
+of the subgoals generated by the previous tactic. This
+covers the frequent cases where a tactic generates two subgoals one of
+which can be easily disposed of.
+
+This is an other powerful way of linearization of scripts, since it
+happens very often that a trivial subgoal can be solved in a less than
+one line tactic. For instance, the tactic:
+
+\begin{center}
+  \ssrN[1]{tactic}\ssrC{; last by} \ssrN[2]{tactic}\ssrC{.}
+\end{center}
+
+tries to solve the last subgoal generated by \ssrN[1]{tactic} using the
+\ssrN[2]{tactic}, and fails if it does not succeeds. Its analogous
+
+\begin{center}
+  \ssrN[1]{tactic}\ssrC{; first by} \ssrN[2]{tactic}.
+\end{center}
+
+tries to solve the first subgoal generated by \ssrN[1]{tactic} using the
+tactic \ssrN[2]{tactic}, and fails if it does not succeeds.
+
+
+\ssr{} also offers an extension of this facility, by supplying
+tactics to \emph{permute}  the subgoals generated by a tactic.
+The tactic:
+
+\begin{center}
+  {\tac}\ssrC{; last first.}
+\end{center}
+
+inverts the order of the subgoals generated by {\tac}. It is
+equivalent to:
+
+\begin{center}
+  {\tac}\ssrC{; first last.}
+\end{center}
+
+
+More generally, the tactic:
+
+\begin{center}
+  {\tac}\ssrC{; last }${\naturalnumber}$ \ssrC{first.}
+\end{center}
+
+where ${\naturalnumber}$ is
+a \Coq{} numeral, or and Ltac variable denoting
+a \Coq{} numeral, having the value $k$. It
+rotates the $n$ subgoals $G_1,
+\dots, G_n$ generated by {\tac}. The first subgoal becomes
+$G_{n + 1 - k}$ and the circular order of subgoals remains unchanged.
+
+Conversely, the tactic:
+
+  {\tac}\ssrC{; first }${\naturalnumber}$ \ssrC{last.}
+
+rotates the $n$ subgoals $G_1,
+\dots, G_n$ generated by \ssrC{tactic} in order that the first subgoal
+becomes $G_{k}$.
+
+Finally, the tactics \ssrC{last} and \ssrC{first} combine with the
+branching syntax of Ltac:
+if the tactic $\ssrN[0]{tactic}$ generates $n$
+subgoals on a given goal, then the tactic
+
+  $tactic_0$\ssrC{; last }${\naturalnumber}$ \ssrC{[}$tactic_1$\ssrC{|}$\dots$\ssrC{|}$tactic_m$\ssrC{] || }$tactic_{m+1}$\ssrC{.}
+
+where ${\naturalnumber}$ denotes the integer $k$ as above, applies $tactic_1$ to the
+$n -k + 1$-th goal, $\dots tactic_m$ to the $n -k + 2 - m$-th
+goal and $tactic_{m+1}$ to the others.
+
+For instance, the script:
+\begin{lstlisting}
+  Inductive test : nat ->  Prop :=
+    C1 : forall n, test n | C2 : forall n, test n |
+    C3 : forall n, test n | C4 : forall n, test n.
+
+  Goal forall n, test n -> True.
+  move=> n t; case: t; last 2 [move=> k| move=> l]; idtac.
+\end{lstlisting}
+
+creates a goal with four subgoals, the first and the last being
+\ssrC{nat -> True}, the second and the third being \ssrC{True} with
+respectively \ssrC{k : nat} and \ssrC{l : nat} in their context.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Iteration}\label{ssec:iter}
+\idx{do \dots{} [ \dots{} ]}
+
+\ssr{} offers an accurate control on the repetition of
+tactics, thanks to the \ssrC{do} tactical, whose general syntax is:
+
+\begin{center}
+	\ssrC{do} \optional{\ssrN{mult}} \ssrC{[} \ssrN[1]{tactic} \ssrC{|} $\dots$ \ssrC{|} \ssrN[n]{tactic} \ssrC{]}
+\end{center}
+where \ssrN{mult} is a \emph{multiplier}.
+
+Brackets can only be omitted if a single tactic is given \emph{and} a
+multiplier is present.
+
+A tactic of the form:
+
+\begin{center}
+  \ssrC{do [} \tac$_1$ \ssrC{|} $\dots$ \ssrC{|} \tac$_n$\ssrC{].}
+\end{center}
+
+is equivalent to the standard Ltac expression:
+
+\begin{center}
+  \ssrC{first [} \tac$_1$ \ssrC{|} $\dots$ \ssrC{|} \tac$_n$\ssrC{].}
+\end{center}
+
+
+The optional multiplier \ssrN{mult} specifies how many times
+the action of {\tac} should be repeated on the current subgoal.
+
+There are four kinds of multipliers:
+  \begin{itemize}
+  \item \ssrC{n!}: the step {\tac} is repeated exactly $n$ times
+    (where $n$ is a positive integer argument).
+  \item \ssrC{!}: the step {\tac} is repeated as many times as possible,
+    and done at least once.
+  \item \ssrC{?}: the step {\tac} is repeated as many times as possible,
+    optionally.
+  \item \ssrC{n?}: the step {\tac} is repeated up to $n$ times,
+    optionally.
+  \end{itemize}
+
+For instance, the tactic:
+
+\begin{center}
+ {\tac} \ssrL+; do 1?rewrite mult_comm.+
+\end{center}
+
+rewrites at most one time the lemma \ssrC{mult_com} in all the subgoals
+generated by {\tac} , whereas the tactic:
+
+\begin{center}
+  {\tac} \ssrL+; do 2!rewrite mult_comm.+
+\end{center}
+
+rewrites exactly two times the lemma \ssrC{mult_com} in all the subgoals
+generated by {\tac}, and fails if this rewrite is not possible
+in some subgoal.
+
+Note that the combination of multipliers and \ssrC{rewrite} is so often
+used that multipliers are in fact integrated to the syntax of the \ssr{}
+\ssrC{rewrite} tactic, see section \ref{sec:rw}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Localization}\label{ssec:gloc}
+\idx{\dots{} in \dots{}}
+
+In sections \ref{ssec:loc} and \ref{ssec:profstack}, we have already
+presented the \emph{localization} tactical \ssrC{in}, whose general
+syntax is:
+\begin{center}
+	{\tac} \ssrC{in} \ssrN{ident}$^+$ \optional{\ssrC{*}}
+\end{center}
+
+where \ssrN{ident}$^+$ is a non empty list of fact
+names in the context. On the left side of \ssrC{in}, {\tac} can be
+\ssrC{move}, \ssrC{case}, \ssrC{elim}, \ssrC{rewrite}, \ssrC{set},
+ or any tactic formed with the general iteration tactical \ssrC{do} (see
+ section \ref{ssec:iter}).
+
+The operation described by {\tac} is performed in the facts
+listed in \ssrN{ident}$^+$ and in the goal if a \ssrC{*} ends
+the list.
+
+The \ssrC{in} tactical successively:
+\begin{itemize}
+\item generalizes the selected hypotheses, possibly ``protecting'' the
+ goal if \ssrC{*} is not present,
+\item performs {\tac}, on the obtained goal,
+\item reintroduces the generalized facts, under the same names.
+\end{itemize}
+
+This defective form of the \ssrC{do} tactical is useful to avoid clashes
+between standard Ltac \ssrC{in} and the \ssr{} tactical \ssrC{in}.
+For example, in the following script:
+\begin{lstlisting}
+  Ltac |*mytac*| H := rewrite H.
+
+  Goal forall x y, x = y -> y = 3 -> x + y  = 6.
+  move=> x y H1 H2.
+  do [mytac H2] in H1 *.
+\end{lstlisting}
+the last tactic rewrites the hypothesis \ssrC{H2 : y = 3} both in
+\ssrC{H1 : x = y} and in the goal \ssrC{x + y = 6}.
+
+By default \ssrC{in} keeps the body of local definitions. To erase
+the body of a local definition during the generalization phase,
+the name of the local definition must be written between parentheses,
+like in \ssrC{rewrite H in H1 (def_n) $\;\;$H2}.
+
+From \ssr{} 1.5 the grammar for the \ssrC{in} tactical has been extended
+to the following one:
+
+\begin{center}
+  {\tac} \ssrC{in} \optional{ 
+	  \ssrN{clear-switch} {\optsep}
+	  \optional{\ssrC{@}}\ssrN{ident} {\optsep}
+          \ssrC{(}\ssrN{ident}\ssrC{)} {\optsep}
+	  \ssrC{(}\optional{\ssrC{@}}\ssrN{ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)}
+		}$^+$ \optional{\ssrC{*}}
+\end{center}
+
+In its simplest form the last option lets one rename hypotheses that can't be
+cleared (like section variables).  For example \ssrC{(y := x)} generalizes
+over \ssrC{x} and reintroduces the generalized
+variable under the name \ssrC{y} (and does not clear \ssrC{x}).\\
+For a more precise description the $\ssrC{(}[\ssrC{@}]\ssrN{ident}\ \ssrC{:=}\ \ssrN{c-pattern}\ssrC{)}$
+item refer to the ``Advanced generalization'' paragraph at page~\pageref{par:advancedgen}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Structure}\label{ssec:struct}
+
+Forward reasoning structures the script by explicitly specifying some
+assumptions to be added to the proof context. It is closely associated
+with the declarative style of proof, since an extensive use of these
+highlighted statements
+make the script closer to a (very detailed) text book proof.
+
+Forward chaining tactics allow to state an intermediate lemma and start a
+piece of script dedicated to the proof of this statement. The use of
+closing tactics (see section \ref{ssec:termin}) and of
+indentation makes syntactically explicit the portion of the script
+building the proof of the intermediate statement.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{have} tactic.}
+\label{sssec:have}
+\idx{have: \dots{}}
+\idx{have: \dots{} := \dots{}}
+
+The main \ssr{} forward reasoning tactic is the \ssrC{have} tactic. It
+can be use in two modes: one starts a new (sub)proof for an
+intermediate result in the main proof, and the other
+provides explicitly a proof term for this intermediate step.
+
+In the first mode, the syntax of \ssrC{have} in its defective form is:
+
+  \ssrC{have: }{\term}\ssrC{.}
+
+This tactic supports open syntax for {\term}.
+Applied to a goal \ssrC{G}, it generates a first subgoal requiring a
+proof of {\term} in the context of \ssrC{G}. The  second generated
+subgoal is of the form {\term} \ssrC{-> G}, where {\term} becomes
+the new top assumption, instead of being introduced with a fresh
+name. At the proof-term level, the \ssrC{have} tactic creates a $\beta$
+redex, and introduces the lemma under a fresh name, automatically
+chosen.
+
+
+Like in the case of the \ssrC{pose} tactic (see section \ref{ssec:pose}),
+the types of the holes are abstracted in {\term}.
+For instance, the tactic:
+\begin{lstlisting}
+  have: _ * 0 = 0.
+\end{lstlisting}
+is equivalent to:
+\begin{lstlisting}
+  have: forall n : nat, n * 0 = 0.
+\end{lstlisting}
+The \ssrC{have} tactic also enjoys the same abstraction mechanism as the
+\ssrC{pose} tactic for the non-inferred implicit arguments. For instance,
+the tactic:
+\begin{lstlisting}
+  have: forall x y, (x, y) = (x, y + 0).
+\end{lstlisting}
+opens a new subgoal to prove that:
+
+\noindent\ssrC{forall (T : Type) (x : T) (y : nat), (x, y) = (x, y + 0)}
+
+
+The behavior of the defective \ssrC{have} tactic makes it possible to
+generalize it in the
+following general construction:
+\begin{center}
+	\ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}}
+	\optional{\ssrN{s-item} {\optsep} \ssrN{binder}$^+$}
+	\optional{\ssrC{:} \ssrN[1]{term}}
+	\optional{\ssrC{:=} \ssrN[2]{term} {\optsep} \ssrC{by} {\tac}}
+\end{center}
+
+Open syntax is supported for $\ssrN[1]{term}$ and $\ssrN[2]{term}$. For the
+description of
+\iitem{}s and clear switches see section \ref{ssec:intro}.
+The first mode of the \ssrC{have} tactic, which opens a sub-proof for an
+intermediate result, uses tactics of the form:
+
+\begin{center}
+  \ssrC{have} \ssrN{clear-switch} \ssrN{i-item} \ssrC{:} {\term} \ssrC{by} {\tac}.
+\end{center}
+
+which behave like:\\
+
+\begin{center}
+  \ssrC{have:} {\term} \ssrC{; first by } {\tac}.
+\end{center}
+\begin{center}
+  \ssrC{  move=>} \ssrN{clear-switch} \ssrN{i-item}.
+\end{center}
+
+
+Note that the \ssrN{clear-switch} \emph{precedes} the
+\ssrN{i-item}, which allows to reuse a name of the context, possibly used
+by the proof of the assumption, to introduce the new assumption
+itself.
+
+The \ssrC{by} feature is especially convenient when the proof script of the
+statement is very short, basically when it fits in one line like in:
+\begin{lstlisting}
+  have H : forall x y, x + y = y + x by move=> x y; rewrite addnC.
+\end{lstlisting}
+
+The possibility of using \iitem{}s supplies a very concise
+syntax for the further use of the intermediate step. For instance,
+\begin{lstlisting}
+  have -> : forall x, x * a = a.
+\end{lstlisting}
+on a goal \ssrC{G}, opens a new subgoal asking for a proof of
+\ssrC{forall x, x * a = a}, and a second subgoal in which the lemma
+ \ssrC{forall x, x * a = a} has been rewritten in the goal \ssrC{G}. Note
+ that in this last subgoal, the intermediate result does not appear in
+ the context.
+Note that, thanks to the deferred execution of clears, the following
+idiom is supported (assuming \ssrC{x} occurs in the goal only):
+\begin{lstlisting}
+  have {x} -> : x = y
+\end{lstlisting}
+
+An other frequent use of the intro patterns combined with \ssrC{have} is the
+destruction of existential assumptions like in the tactic:
+\begin{lstlisting}
+  have [x Px]: exists x : nat, x > 0.
+\end{lstlisting}
+which opens a new subgoal asking for a proof of \ssrC{exists x : nat, x >
+  0} and  a second subgoal in which the witness is introduced under
+the name \ssrC{x : nat}, and its property under the name \ssrC{Px : x > 0}.
+
+An alternative use of the \ssrC{have} tactic is to provide the explicit proof
+term for the intermediate lemma, using tactics of the form:
+
+\begin{center}
+  \ssrC{have} \optional{\ssrN{ident}} \ssrC{:=} {\term}.
+\end{center}
+
+This tactic creates a new assumption of type the type of
+{\term}. If the
+optional \ssrN{ident} is present, this assumption is introduced under
+the name \ssrN{ident}. Note that the body of the constant is lost for
+the user.
+
+Again, non inferred implicit arguments and explicit holes are abstracted. For
+instance, the tactic:
+\begin{lstlisting}
+  have H := forall x, (x, x) = (x, x).
+\end{lstlisting}
+adds to the context \ssrC{H : Type -> Prop}. This is a schematic example but
+the feature is specially useful when the proof term to give involves
+for instance a lemma with some hidden implicit arguments.
+
+After the \ssrN{i-pattern}, a list of binders is allowed.
+For example, if \ssrC{Pos_to_P} is a lemma that proves that
+\ssrC{P} holds for any positive, the following command:
+\begin{lstlisting}
+  have H x (y : nat) : 2 * x + y = x + x + y by auto.
+\end{lstlisting}
+will put in the context \ssrC{H : forall x, 2 * x = x + x}. A proof term
+provided after \ssrC{:=} can mention these bound variables (that are
+automatically introduced with the given names).
+Since the \ssrN{i-pattern} can be omitted, to avoid ambiguity, bound variables
+can be surrounded with parentheses even if no type is specified:
+\begin{lstlisting}
+  have (x) : 2 * x = x + x by auto.
+\end{lstlisting}
+
+The \ssrN{i-item}s and \ssrN{s-item} can be used to interpret the
+asserted hypothesis with views (see section~\ref{sec:views}) or
+simplify the resulting goals.
+
+The \ssrC{have} tactic also supports a \ssrC{suff} modifier which allows for
+asserting that a given statement implies the current goal without
+copying the goal itself. For example, given a goal \ssrC{G} the tactic
+\ssrC{have suff H : P} results in the following two goals:
+\begin{lstlisting}
+   |- P -> G
+   H : P -> G |- G
+\end{lstlisting}
+Note that \ssrC{H} is introduced in the second goal. The \ssrC{suff}
+modifier is not compatible with the presence of a list of binders.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Generating \ssrC{let in} context entries with \ssrC{have}}
+\label{sec:havetransparent}
+
+Since \ssr{} 1.5 the \ssrC{have} tactic supports a ``transparent'' modifier to
+generate \ssrC{let in} context entries: the \ssrC{@} symbol in front of the context
+entry name.  For example:
+
+\begin{lstlisting}
+have @i : 'I_n by apply: (Sub m); auto.
+\end{lstlisting}
+generates the following two context entry:
+\begin{lstlisting}
+i := Sub m proof_produced_by_auto : 'I_n
+\end{lstlisting}
+
+Note that the sub-term produced by \ssrC{auto} is in general huge and
+uninteresting, and hence one may want to hide it.
+
+For this purpose the \ssrC{[: name ]} intro pattern and the tactic
+\ssrC{abstract} (see page~\pageref{ssec:abstract}) are provided.
+Example:
+\begin{lstlisting}
+have [:blurb] @i : 'I_n by apply: (Sub m); abstract: blurb; auto.
+\end{lstlisting}
+generates the following two context entries:
+\begin{lstlisting}
+blurb : (m < n) (*1*)
+i := Sub m blurb : 'I_n
+\end{lstlisting}
+The type of \ssrC{blurb} can be cleaned up by its annotations by just simplifying
+it.  The annotations are there for technical reasons only.
+
+When intro patterns for abstract constants are used in conjunction
+with \ssrC{have} and an explicit term, they must be used as follows:
+
+\begin{lstlisting}
+have [:blurb] @i : 'I_n := Sub m blurb.
+  by auto.
+\end{lstlisting}
+
+In this case the abstract constant \ssrC{blurb} is assigned by using it
+in the term that follows \ssrC{:=} and its corresponding goal is left to
+be solved.  Goals corresponding to intro patterns for abstract constants
+are opened in the order in which the abstract constants are declared (not
+in the ``order'' in which they are used in the term).
+
+Note that abstract constants do respect scopes.  Hence, if a variable
+is declared after their introduction, it has to be properly generalized (i.e.
+explicitly passed to the abstract constant when one makes use of it).
+For example any of the following two lines:
+\begin{lstlisting}
+have [:blurb] @i k : 'I_(n+k) by apply: (Sub m); abstract: blurb k; auto.
+have [:blurb] @i k : 'I_(n+k) := apply: Sub m (blurb k); first by auto.
+\end{lstlisting}
+generates the following context:
+\begin{lstlisting}
+blurb : (forall k, m < n+k) (*1*)
+i := fun k => Sub m (blurb k) : forall k, 'I_(n+k)
+\end{lstlisting}
+
+Last, notice that the use of intro patterns for abstract constants is
+orthogonal to the transparent flag \ssrC{@} for \ssrC{have}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{The \ssrC{have} tactic and type classes resolution}
+\label{ssec:havetcresolution}
+
+Since \ssr{} 1.5 the \ssrC{have} tactic behaves as follows with respect to type
+classes inference.
+
+\begin{itemize}
+\item \ssrC{have foo : ty.}
+	Full inference for \ssrC{ty}.
+	The first subgoal demands a proof of such instantiated statement.
+\item \ssrC{have foo : ty := .}
+	No inference for \ssrC{ty}. Unresolved instances are quantified in
+	\ssrC{ty}.  The first subgoal demands a proof of such quantified
+	statement.  Note that no proof term follows \ssrC{:=}, hence two
+	subgoals are generated.
+\item \ssrC{have foo : ty := t.}
+	No inference for \ssrC{ty} and \ssrC{t}.
+\item \ssrC{have foo := t.}
+	No inference for \ssrC{t}. Unresolved instances are quantified in the
+	(inferred) type of \ssrC{t} and abstracted in \ssrC{t}.
+\end{itemize}
+
+The behavior of \ssr{} 1.4 and below (never resolve type classes)
+can be restored with the option \ssrC{Set SsrHave NoTCResolution}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Variants: the \ssrC{suff} and  \ssrC{wlog} tactics.}
+\label{ssec:wlog}
+\idx{suff: \dots{}}
+\idx{suffices: \dots{}}
+\idx{wlog: \dots{} / \dots{}}
+\idx{without loss: \dots{} / \dots{}}
+
+As it is often the case  in mathematical textbooks, forward
+reasoning may be used in slightly different variants.
+One of these variants is to show that the intermediate step $L$
+easily implies the initial goal $G$. By easily we mean here that
+the proof of $L \Rightarrow G$ is shorter than the one of $L$
+itself. This kind of reasoning step usually starts with:
+``It suffices to show that \dots''.
+
+This is such a frequent way of reasoning that \ssr{} has a variant of the
+\ssrC{have} tactic called \ssrC{suffices} (whose abridged name is
+\ssrC{suff}). The \ssrC{have} and \ssrC{suff} tactics are equivalent and
+have the same syntax but:
+\begin{itemize}
+\item the order of the generated subgoals is inversed
+\item but the optional clear item is still performed in the
+  \emph{second} branch. This means that the tactic:
+\begin{lstlisting}
+  suff {H} H : forall x : nat, x >= 0.
+\end{lstlisting}
+fails if the context of the current goal indeed contains an
+assumption named \ssrC{H}.
+\end{itemize}
+The rationale of this clearing policy is to make possible ``trivial''
+refinements of an assumption, without changing its name in the main
+branch of the reasoning.
+
+The \ssrC{have} modifier can follow the \ssrC{suff} tactic.
+For example, given a goal \ssrC{G} the tactic
+\ssrC{suff have H : P} results in the following two goals:
+\begin{lstlisting}
+  H : P |- G
+  |- (P -> G) -> G
+\end{lstlisting}
+Note that, in contrast with \ssrC{have suff}, the name \ssrC{H} has been introduced
+in the first goal.
+
+Another useful construct is reduction,
+showing that a particular case is in fact general enough to prove
+a general property. This kind of reasoning step usually starts with:
+``Without loss of generality, we can suppose that \dots''.
+Formally, this corresponds to the proof of a goal \ssrC{G} by introducing
+a cut \ssrN{wlog\_statement} \ssrC{-> G}. Hence the user shall provide a
+proof for both \ssrC{(}\ssrN{wlog\_statement} \ssrC{-> G) -> G} and
+\ssrN{wlog\_statement} \ssrC{-> G}. However, such cuts are usually rather
+painful to perform by hand, because the statement
+\ssrN{wlog\_statement} is tedious to write by hand, and somtimes even
+to read.
+
+\ssr{} implements this kind of reasoning step through the \ssrC{without loss}
+tactic, whose short name is \ssrC{wlog}. It offers support to describe
+the shape of the cut statements, by providing the simplifying
+hypothesis and by pointing at the elements of the initial goals which
+should be generalized. The general syntax of \ssrC{without loss} is:
+
+\begin{center}
+  \ssrC{wlog} \optional{\ssrC{suff}} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-item}} \ssrC{:} \optional{\ssrN[1]{ident} $\dots$ \ssrN[n]{ident}} \ssrC{/} {\term}
+\end{center}
+
+where \ssrN[1]{ident} $\dots$ \ssrN[n]{ident} are identifiers for constants
+in the context of the goal. Open syntax is supported for {\term}.
+
+In its defective form:
+
+\begin{center}
+  \ssrC{wlog: /} {\term}.
+\end{center}
+
+on a goal \ssrC{G}, it creates two subgoals: a first one to prove the formula
+\ssrC{(}{\term} \ssrC{-> G) -> G} and a second one to prove the formula
+{\term} \ssrC{-> G}.
+
+:browse confirm wa
+If the optional list \ssrN[1]{ident} $\dots$ \ssrN[n]{ident} is present on the left
+side of \ssrC{/}, these constants are generalized in the premise
+\ssrC{(}{\term} \ssrC{-> G)} of the first subgoal. By default the body of
+local definitions  is erased. This behavior can be inhibited
+prefixing the name of the local definition with the \ssrC{@} character.
+
+In the second subgoal, the tactic:
+
+\begin{center}
+  \ssrC{move=>} \ssrN{clear-switch}\ssrC{} \ssrN{i-item}\ssrC{.}
+\end{center}
+
+is performed if at least one of these optional switches is present in
+the \ssrC{wlog} tactic.
+
+The \ssrC{wlog} tactic is specially useful when a symmetry argument
+simplifies a proof. Here is an example showing the beginning of the
+proof that quotient and reminder of natural number euclidean division
+are unique.
+\begin{lstlisting}
+  Lemma quo_rem_unicity: forall d q1 q2 r1 r2,
+     q1*d + r1 = q2*d + r2 -> r1 < d -> r2 < d -> (q1, r1) =  (q2, r2).
+  move=> d q1 q2 r1 r2.
+  wlog: q1 q2 r1 r2 / q1 <= q2.
+    by case (le_gt_dec q1 q2)=> H; last symmetry; eauto with arith.
+\end{lstlisting}
+
+The \ssrC{wlog suff} variant is simpler, since it cuts
+\ssrN{wlog\_statement} instead of \ssrN{wlog\_statement} \ssrC{-> G}. It thus
+opens the goals \ssrN{wlog\_statement} \ssrC{-> G} and \ssrN{wlog\_statement}.
+
+In its simplest form
+the \ssrC{generally have :...} tactic
+is equivalent to \ssrC{wlog suff :...} followed by \ssrC{last first}.
+When the \ssrC{have} tactic
+is used with the \ssrC{generally} (or \ssrC{gen}) modifier it accepts an
+extra identifier followed by a comma before the usual intro pattern.
+The identifier will name the new hypothesis in its more general form,
+while the intro pattern will be used to process its instance.  For example:
+\begin{lstlisting}
+  Lemma simple n (ngt0 : 0 < n ) : P n.
+  gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0).
+\end{lstlisting}
+The first subgoal will be
+\begin{lstlisting}
+  n : nat
+  ngt0 : 0 < n
+  ====================
+  (0 <= n) && (n != 0)
+\end{lstlisting}
+while the second one will be
+\begin{lstlisting}
+  n : nat
+  ltnV : forall n, 0 < n -> (0 <= n) && (n != 0)
+  nge0 : 0 <= n
+  neqn0 : n != 0
+  ====================
+  P n
+\end{lstlisting}
+
+\paragraph{Advanced generalization}\label{par:advancedgen}
+The complete syntax for the items on the left hand side of the \ssrC{/}
+separator is the following one:
+\begin{center}
+\ssrN{clear-switch} {\optsep} \optional{\ssrC{@}} \ssrN{ident} {\optsep} \ssrC{(}\optional{\ssrC{@}}\ssrN{ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)}
+\end{center}
+Clear operations are intertwined with generalization operations. This
+helps in particular avoiding dependency issues while generalizing some facts.
+
+\noindent
+If an \ssrN{ident} is prefixed with the \ssrC{@} prefix mark, then a
+let-in redex is created, which keeps track if its body (if any). The
+syntax \ssrC{(}\ssrN{ident}\ssrC{:=}\ssrN{c-pattern}\ssrC{)} allows to
+generalize an arbitrary term using a given name.  Note that its simplest
+form \ssrC{(x := y)} is just a renaming of \ssrC{y} into \ssrC{x}. In
+particular, this can be useful in order to simulate the generalization
+of a section variable, otherwise not allowed. Indeed renaming does not
+require the original variable to be cleared.
+
+
+\noindent
+The syntax \ssrC{(@x := y)} generates a let-in abstraction but with the following
+caveat: \ssrC{x} will not bind \ssrC{y}, but its body, whenever \ssrC{y} can be
+unfolded. This cover the case of both local and global definitions, as
+illustrated in the following example:
+
+\begin{lstlisting}
+Section Test.
+Variable x : nat.
+Definition addx z := z + x.
+Lemma test : x <= addx x.
+wlog H : (y := x) (@twoy := addx x) / twoy = 2 * y.
+\end{lstlisting}
+\noindent
+The first subgoal is:
+\begin{lstlisting}
+   (forall y : nat, let twoy := y + y in twoy = 2 * y -> y <= twoy) ->
+   x <= addx x
+\end{lstlisting}
+\noindent
+To avoid unfolding the term captured by the pattern \ssrC{add x} one
+can use the pattern \ssrC{id (addx x)}, that would produce the following first
+subgoal:
+\begin{lstlisting}
+   (forall y : nat, let twoy := addx y in twoy = 2 * y -> y <= twoy) ->
+   x <= addx x
+\end{lstlisting}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Rewriting}\label{sec:rw}
+\idx{rewrite \dots{}}
+
+The generalized use of reflection implies that most of the
+intermediate results handled are properties of effectively computable
+functions. The most efficient mean of establishing such results are
+computation and simplification of expressions involving such
+functions, i.e., rewriting. \ssr{} therefore includes an extended
+\ssrC{rewrite} tactic, that unifies and combines most of the rewriting
+functionalities.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{An extended \ssrC{rewrite} tactic}\label{ssec:extrw}
+The main features of the \ssrC{rewrite} tactic are:
+\begin{itemize}
+\item  It can perform an entire series of such operations in any
+  subset of the goal and/or context;
+\item It allows to perform rewriting,
+  simplifications, folding/unfolding of definitions, closing of goals;
+\item Several rewriting operations can be chained in a single tactic;
+\item Control over the occurrence at which rewriting is to be performed is
+  significantly enhanced.
+\end{itemize}
+
+
+The general form of an \ssr{} rewrite tactic is:
+
+\begin{center}
+   \ssrC{rewrite} \ssrN{rstep}$^+$\ssrC{.}
+\end{center}
+
+The combination of a rewrite tactic with the \ssrC{in} tactical (see
+section \ref{ssec:loc}) performs rewriting in both the context and the
+goal.
+
+A rewrite step \ssrN{rstep} has the general form:
+
+\begin{center}
+  \optional{\ssrN{r-prefix}}\ssrN{r-item}
+\end{center}
+
+where:
+
+\begin{longtable}{rcl}
+\ssrN{r-prefix} & ::= &
+	\optional{\ssrC{-}} \optional{\ssrN{mult}} \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{\ssrC{[}\ssrN{r-pattern}\ssrC{]}}\\
+\ssrN{r-pattern} & ::= &
+{\term} {\optsep} \ssrC{in} \optional{\ssrN{ident} \ssrC{in}} {\term} {\optsep} \optional{{\term} \ssrC{in} {\optsep} {\term} \ssrC{as} } \ssrN{ident} \ssrC{in} {\term}\\
+\ssrN{r-item} & ::= &
+\optional{\ssrC{/}}{\term} {\optsep} \ssrN{s-item} \\
+\end{longtable}
+
+
+% \begin{eqnarray*}
+% \ssrN{r-prefix} & ::= &
+% [\ssrC{-}]\ [\ssrN{mult}][\ssrN{occ-switch} | \ssrN{cl-item}][{\term}]\\
+% \ssrN{r-item} & ::= &
+% [\ssrC{-}]{\term}\ |\ [\ssrC{-}]\ssrC{[}\ssrN[1]{term}\ssrC{]}\ssrC{/(}\ssrN[2]{term}\ssrC{)} \ |\
+% \ssrN{simpl switch} \ |\  \\
+% && \ssrN{eq-term} \ |\  \ssrC{(} \ssrN[1]{eq-term}\ssrC{,}\dots
+% \ssrC{,}\ssrN[n]{eq-term} \ssrC{)} \ |\  \ssrC{(_ :}\ssrN{eq-term} \ssrC{)}
+% \end{eqnarray*}
+
+
+An \ssrN{r-prefix} contains annotations to qualify where and how   the
+rewrite operation should be performed:
+\begin{itemize}
+\item The optional initial \ssrC{-} indicates the direction of the rewriting
+  of \ssrN{r-item}: if present the direction is right-to-left and it is
+  left-to-right otherwise.
+\item The multiplier \ssrN{mult} (see section \ref{ssec:iter})
+  specifies if and how the rewrite operation should be repeated.
+\item A rewrite operation matches the occurrences of a \emph{rewrite
+  pattern}, and replaces these occurrences by an other term, according
+  to the given \ssrN{r-item}.
+  The optional \emph{redex switch} $\ssrC{[}\ssrN{r-pattern}\ssrC{]}$, which
+  should always be surrounded by brackets, gives explicitly this
+  rewrite pattern. In its simplest form, it is a regular term.
+  If no explicit redex switch
+  is present the rewrite pattern to be matched is inferred from the
+  \ssrN{r-item}.
+\item This optional {\term}, or
+  the \ssrN{r-item}, may be preceded by an
+  occurrence switch (see section \ref{ssec:select}) or a clear item
+  (see section \ref{ssec:discharge}), these two possibilities being
+  exclusive. An occurrence switch selects the occurrences of the
+  rewrite pattern which should be affected by the rewrite operation.
+\end{itemize}
+
+
+An \ssrN{r-item} can be:
+
+
+\begin{itemize}
+\item A \emph{simplification r-item}, represented by a
+  \ssrN{s-item} (see section \ref{ssec:intro}).
+% In some cases, \ssrN{r-prefix}es are not supported.
+  Simplification operations are
+  intertwined with the possible other rewrite operations specified by
+  the list of r-items.
+\item A \emph{folding/unfolding r-item}. The tactic:
+
+  \ssrC{rewrite /}{\term}
+
+unfolds the head constant of \textit{term} in every occurrence of the
+first matching of \textit{term} in the goal. In particular, if
+\ssrC{my_def} is a (local or global) defined constant, the tactic:
+\begin{lstlisting}
+  rewrite /my_def.
+\end{lstlisting}
+is analogous to:
+\begin{lstlisting}
+  unfold my_def.
+\end{lstlisting}
+Conversely:
+\begin{lstlisting}
+  rewrite -/my_def.
+\end{lstlisting}
+is equivalent to:
+\begin{lstlisting}
+  fold my_def.
+\end{lstlisting}
+%\emph{Warning} The combination of redex switch with unfold
+%\ssrN{r-item} is not yet implemented.
+
+When an unfold r-item is combined with a redex pattern, a conversion
+operation is performed. A tactic of the form:
+
+\begin{center}
+  \ssrC{rewrite -[}\ssrN[1]{term}\ssrC{]/}\ssrN[2]{term}\ssrC{.}
+\end{center}
+
+is equivalent to:
+
+
+\begin{center}
+  \ssrC{change} \ssrN[1]{term} \ssrC{with} \ssrN[2]{term}\ssrC{.}
+\end{center}
+
+
+If \ssrN[2]{term} is a single constant and \ssrN[1]{term} head symbol
+is not \ssrN[2]{term}, then the head symbol of \ssrN[1]{term} is
+repeatedly unfolded until \ssrN[2]{term} appears.
+
+\begin{lstlisting}
+  Definition double x := x + x.
+  Definition ddouble x := double (double x).
+  Lemma ex1 x : ddouble x = 4 * x.
+  rewrite [ddouble _]/double.
+\end{lstlisting}
+
+The resulting goal is:
+
+\begin{lstlisting}
+  double x + double x = 4 * x
+\end{lstlisting}
+
+\emph{Warning} The \ssr{} terms containing holes are \emph{not}
+typed as abstractions in this context. Hence the following script:
+\begin{lstlisting}
+  Definition f := fun x y => x + y.
+  Goal forall x y, x +  y = f y x.
+  move=> x y.
+  rewrite -[f y]/(y + _).
+\end{lstlisting}
+raises the error message
+\begin{verbatim}
+   User error: fold pattern (y + _) does not match redex (f y)
+\end{verbatim}
+but the script obtained by replacing the last line with:
+\begin{lstlisting}
+  rewrite -[f y x]/(y + _).
+\end{lstlisting}
+is valid.
+
+
+\item A term, which can be:
+  \begin{itemize}
+    \item A term whose type has the form:
+      $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$
+      where $eq$ is the Leibniz equality or a registered setoid
+      equality. %In the case of setoid relations, the only supported
+      %r-prefix is the directional \ssrC{-}.
+    \item A list of terms $(t_1,\dots,t_n)$, each $t_i$ having a type of the
+      form: $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$ where
+      $eq$ is the Leibniz equality or a registered setoid
+      equality. The tactic:
+
+        \centerline{\ssrC{rewrite} \ssrN{r-prefix}\ssrC{(}$t_1$\ssrC{,}$\dots$\ssrC{,}$t_n$\ssrC{).}}
+
+      is equivalent to:
+
+  \centerline{\ssrC{do [rewrite} \ssrN{r-prefix} $t_1$ \ssrC{|} $\dots$ \ssrC| rewrite} \ssrN{r-prefix} $t_n$\ssrC{].}
+
+    \item An anonymous rewrite lemma
+      \ssrC{(_ :} {\term}), where \textit{term} has again the form:
+      $$\ssrC{forall}\ (x_1\ :\ A_1)\dots(x_n\ :\ A_n),\ eq\ term_1\ term_2$$
+      The tactic:
+
+        \centerline{\ssrC{rewrite (_ :} {\term}\ssrC{)}}
+
+      is in fact synonym of:
+
+        \centerline{\ssrC{cutrewrite (}{\term}\ssrC{).}}
+
+
+  \end{itemize}
+
+\end{itemize}
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Remarks and examples}\label{ssec:rwex}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Rewrite redex selection}
+The general strategy of \ssr{}
+is to grasp as many redexes as possible and to let the user select the
+ones to be rewritten thanks to the improved syntax for the control of
+rewriting.
+
+This may be a source of incompatibilities between the two \ssrC{rewrite}
+tactics.
+
+In a rewrite tactic of the form:
+
+  \ssrC{rewrite} \ssrN{occ-switch}\ssrC{[}\ssrN[1]{term}\ssrC{]}\ssrN[2]{term}.
+
+\ssrN[1]{term} is the explicit rewrite redex and
+\ssrN[2]{term} is the
+rewrite rule. This execution of this tactic unfolds as follows:
+
+\begin{itemize}
+\item First \ssrN[1]{term} and \ssrN[2]{term} are $\beta\iota$ normalized. Then
+  \ssrN[2]{term} is put in head normal form if the Leibniz equality
+  constructor \ssrC{eq} is not the head symbol. This may involve $\zeta$
+  reductions.
+\item Then, the matching algorithm (see section \ref{ssec:set})
+  determines the first subterm of the goal matching the rewrite pattern.
+  The rewrite pattern is
+  given by \ssrN[1]{term}, if an explicit redex pattern switch is provided, or by
+  the type of \ssrN[2]{term} otherwise. However, matching skips over
+  matches that would lead to trivial rewrites. All the
+  occurrences of this subterm in the goal are candidates for rewriting.
+\item Then only the occurrences coded by \ssrN{occ-switch} (see again
+  section \ref{ssec:set}) are finally selected for rewriting.
+\item The left hand side of $\ssrN[2]{term}$ is unified with the subterm found
+  by the matching algorithm, and if this succeeds, all the selected
+  occurrences in the goal are replaced by the right hand side of
+  $\ssrN[2]{term}$.
+\item Finally the goal is $\beta\iota$ normalized.
+\end{itemize}
+
+In the case $\ssrN[2]{term}$ is a list of terms, the first top-down (in
+the goal) left-to-right (in the list) matching rule gets selected.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Chained rewrite steps}
+
+
+The possibility to chain rewrite operations in a single tactic makes
+scripts more compact and gathers in a single command line a bunch
+of surgical
+operations  which would be described by a one sentence in a pen and
+paper proof.
+
+Performing rewrite and simplification operations in a single tactic
+enhances significantly the concision of scripts. For instance the
+tactic:
+\begin{lstlisting}
+  rewrite /my_def {2}[f _]/= my_eq //=.
+\end{lstlisting}
+unfolds \ssrC{my_def} in the goal, simplifies the second occurrence of the
+first subterm matching pattern \ssrC{[f _]}, rewrites \ssrC{my_eq},
+simplifies the whole goal and closes trivial goals.
+
+Here are some concrete examples of chained rewrite operations, in the
+proof of basic results on natural numbers arithmetic:
+
+\begin{lstlisting}
+  Lemma |*addnS*| : forall m n, m + n.+1 = (m + n).+1.
+  Proof. by move=> m n; elim: m. Qed.
+
+  Lemma |*addSnnS*| : forall m n, m.+1 + n = m + n.+1.
+  Proof. move=> *; rewrite addnS; apply addSn. Qed.
+
+  Lemma |*addnCA*| : forall m n p, m + (n + p) = n + (m + p).
+  Proof. by move=> m n; elim: m => [|m Hrec] p; rewrite ?addSnnS -?addnS. Qed.
+
+  Lemma |*addnC*| : forall m n, m + n = n + m.
+  Proof. by move=> m n; rewrite -{1}[n]addn0 addnCA addn0. Qed.
+\end{lstlisting}
+
+Note the use of the \ssrC{?} switch for parallel rewrite operations in
+the proof of \ssrC{|*addnCA*|}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Explicit redex switches are matched first}
+If an \ssrN{r-prefix} involves a \emph{redex switch}, the first step is to
+find a subterm matching this redex pattern, independently from the left hand
+side \ssrC{t1} of the equality the user wants to rewrite.
+
+For instance, if \ssrL-H : forall t u, t + u = u + t- is in the context of a
+goal \ssrL-x + y = y + x-, the tactic:
+\begin{lstlisting}
+  rewrite [y + _]H.
+\end{lstlisting}
+transforms the goal into \ssrL-x + y = x + y-.
+
+Note that if this first pattern matching is not compatible with the
+\emph{r-item}, the rewrite fails, even if the goal contains a correct
+redex matching both the redex switch and the left hand side of the
+equality. For instance, if \ssrL-H : forall t u, t + u * 0 = t- is
+in the context of a goal \ssrL-x + y * 4 + 2 * 0 = x + 2 * 0-, then tactic:
+\begin{lstlisting}
+  rewrite [x + _]H.
+\end{lstlisting}
+raises the error message:
+\begin{verbatim}
+  User error: rewrite rule H doesn't match redex (x + y * 4)
+\end{verbatim}
+while the tactic:
+\begin{lstlisting}
+  rewrite (H _ 2).
+\end{lstlisting}
+transforms the goal into \ssrL-x + y * 4 = x + 2 * 0-.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Occurrence switches and redex switches}
+The tactic:
+\begin{lstlisting}
+  rewrite {2}[_ + y + 0](_: forall z, z + 0 = z).
+\end{lstlisting}
+transforms the goal:
+\begin{lstlisting}
+  x + y + 0 = x + y + y + 0 + 0 + (x + y + 0)
+\end{lstlisting}
+into:
+\begin{lstlisting}
+  x + y + 0 = x + y + y + 0 + 0 + (x + y)
+\end{lstlisting}
+and generates a second subgoal:
+\begin{lstlisting}
+  forall z : nat, z + 0 = z
+\end{lstlisting}
+The second subgoal is generated by the use of an anonymous lemma in
+the rewrite tactic. The effect of the tactic on the initial goal is to
+rewrite this lemma at the second occurrence of the first matching
+\ssrL-x + y + 0- of the explicit rewrite redex \ssrL-_ + y + 0-.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Occurrence selection and repetition}
+Occurrence selection has priority over repetition switches. This means
+the repetition of a rewrite tactic specified by a multiplier
+will perform matching each time an elementary rewrite operation is
+performed. Repeated rewrite tactics apply to every subgoal generated
+by the previous tactic, including the previous instances of the
+repetition. For example:
+\begin{lstlisting}
+  Goal forall x y z : nat,  x + 1 = x + y + 1.
+  move=> x y z.
+\end{lstlisting}
+creates a goal \ssrC{ x + 1 = x + y + 1}, which is turned into \ssrC{z = z}
+by the additional tactic:
+\begin{lstlisting}
+  rewrite 2!(_ : _ + 1 = z).
+\end{lstlisting}
+In fact, this last tactic generates \emph{three} subgoals,
+respectively
+\ssrC{ x + y + 1 = z}, \ssrC{ z = z} and \ssrC{x + 1 = z}. Indeed, the second
+rewrite operation specified with the \ssrC{2!} multiplier applies to
+the two subgoals generated by the first rewrite.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Multi-rule rewriting}
+The \ssrC{rewrite} tactic can be provided a \emph{tuple} of rewrite rules,
+or more generally a tree of such rules, since this tuple can feature
+arbitrary inner parentheses. We call \emph{multirule} such a
+generalized rewrite rule. This feature is of special interest when it
+is combined with  multiplier switches, which makes the \ssrC{rewrite}
+tactic iterates the rewrite operations prescribed by the rules on the
+current goal. For instance, let us define two triples \ssrC{multi1} and
+\ssrC{multi2} as:
+\begin{lstlisting}
+  Variables (a b c : nat).
+
+  Hypothesis eqab : a = b.
+
+  Hypothesis eqac : a = c.
+\end{lstlisting}
+
+Executing the tactic:
+\begin{lstlisting}
+  rewrite (eqab, eqac)
+\end{lstlisting}
+on the goal:
+\begin{lstlisting}
+  =========
+  a = a
+\end{lstlisting}
+turns it into \ssrC{b = b}, as rule \ssrC{eqab} is the first to apply among
+the ones gathered in the tuple passed to the \ssrC{rewrite}
+tactic. This multirule \ssrC{(eqab, eqac)} is actually a \Coq{} term and we
+can name it with a definition:
+\begin{lstlisting}
+Definition |*multi1*| := (eqab, eqac).
+\end{lstlisting}
+In this case, the tactic \ssrC{rewrite multi1} is a synonym for
+\ssrC{(eqab, eqac)}. More precisely, a multirule rewrites
+the first subterm to which one of the rules applies in a left-to-right
+traversal of the goal, with the first rule from the multirule tree in
+left-to-right order. Matching is performed according to the algorithm
+described in Section~\ref{ssec:set}, but literal matches have
+priority. For instance if we add a definition and a new multirule to
+our context:
+
+\begin{lstlisting}
+  Definition |*d*| := a.
+
+  Hypotheses eqd0 : d = 0.
+
+  Definition |*multi2*| := (eqab, eqd0).
+\end{lstlisting}
+then executing the tactic:
+\begin{lstlisting}
+   rewrite multi2.
+\end{lstlisting}
+on the goal:
+\begin{lstlisting}
+  =========
+  d = b
+\end{lstlisting}
+turns it into \ssrC{0 = b}, as rule \ssrC{eqd0} applies without unfolding
+the definition of \ssrC{d}.  For repeated rewrites the selection process
+is repeated anew. For instance, if we define:
+
+\begin{lstlisting}
+   Hypothesis eq_adda_b : forall x, x + a = b.
+
+   Hypothesis eq_adda_c : forall x, x + a = c.
+
+   Hypothesis eqb0 : b = 0.
+
+   Definition |*multi3*| := (eq_adda_b, eq_adda_c, eqb0).
+\end{lstlisting}
+then executing the tactic:
+\begin{lstlisting}
+  rewrite 2!multi3.
+\end{lstlisting}
+on the goal:
+\begin{lstlisting}
+  =========
+  1 + a = 12 + a
+\end{lstlisting}
+turns it into \ssrC{0 = 12 + a}: it uses \ssrC{eq_adda_b} then \ssrC{eqb0} on the
+left-hand side only. Now executing the tactic \ssrC{rewrite !multi3}
+turns the same goal into \ssrC{0 = 0}.
+
+The grouping of rules inside a multirule does not affect the selection
+strategy but can make it easier to include one rule set in another or
+to (universally) quantify over the parameters of a subset of rules (as
+there is special code that will omit unnecessary quantifiers for rules that
+can be syntactically extracted). It is also possible to
+reverse the direction of a rule subset, using a special dedicated syntax:
+the tactic \ssrC{rewrite (=~ multi1)} is equivalent to
+\ssrC{rewrite multi1_rev} with:
+\begin{lstlisting}
+  Hypothesis eqba : b = a.
+
+  Hypothesis eqca : c = a.
+
+  Definition |*multi1_rev*| := (eqba, eqca).
+\end{lstlisting}
+except that the constants \ssrC{eqba, eqab, mult1_rev} have not been created.
+
+Rewriting with multirules
+is useful to implement simplification or transformation
+procedures, to be applied on terms of small to medium size. For
+instance the library \ssrL{ssrnat} provides two implementations for
+arithmetic operations on natural numbers: an elementary one and a tail
+recursive version, less inefficient but also less convenient for
+reasoning purposes. The library also provides one lemma per such
+operation, stating that both versions return the same values when
+applied to the same arguments:
+
+\begin{lstlisting}
+  Lemma |*addE*| : add =2 addn.
+  Lemma |*doubleE*| : double =1 doublen.
+  Lemma |*add_mulE*| n m s : add_mul n m s = addn (muln n m) s.
+  Lemma |*mulE*| : mul =2 muln.
+  Lemma |*mul_expE*| m n p : mul_exp m n p = muln (expn m n) p.
+  Lemma |*expE*| : exp =2 expn.
+  Lemma |*oddE*| : odd =1 oddn.
+\end{lstlisting}
+
+The operation on the left hand side of each lemma is the efficient
+version, and the corresponding naive implementation is on the right
+hand side. In order to reason conveniently on expressions involving
+the efficient operations, we gather all these rules in the
+definition \ssrC{|*trecE*|}:
+\begin{lstlisting}
+ Definition |*trecE*| := (addE, (doubleE, oddE), (mulE, add_mulE, (expE, mul_expE))).
+\end{lstlisting}
+The tactic:
+\begin{lstlisting}
+  rewrite !trecE.
+\end{lstlisting}
+restores the naive versions of each operation in a goal involving the
+efficient ones, e.g. for the purpose of a correctness proof.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Wildcards vs abstractions}
+     The \ssrC{rewrite} tactic supports r-items containing holes. For example
+      in the tactic $(1)$:
+\begin{lstlisting}
+  rewrite (_ : _ * 0 = 0).
+\end{lstlisting}
+      the term \ssrC{_ * 0 = 0} is interpreted as \ssrC{forall n : nat, n * 0 = 0}.
+      Anyway this tactic is \emph{not} equivalent to the tactic $(2)$:
+\begin{lstlisting}
+  rewrite (_ : forall x, x * 0 = 0).
+\end{lstlisting}
+      The tactic $(1)$ transforms the goal
+      \ssrL-(y * 0) + y * (z * 0) = 0- into \ssrC{y * (z * 0) = 0}
+      and generates a new subgoal to prove the statement \ssrC{y * 0 = 0},
+      which is the \emph{instance} of the\\ \ssrC{forall x, x * 0 = 0}
+      rewrite rule that
+      has been used to perform the rewriting. On the other hand, tactic
+      $(2)$ performs the same rewriting on the current goal but generates a
+      subgoal to prove \ssrC{forall x, x * 0 = 0}.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{When \ssr{} \ssrC{rewrite} fails on standard \Coq{} licit rewrite}
+In a few cases, the \ssr{} \ssrC{rewrite} tactic fails
+rewriting some redexes which standard \Coq{} successfully rewrites.
+There are two main cases:
+
+\begin{itemize}
+\item \ssr{} never accepts to rewrite indeterminate patterns like:
+\begin{lstlisting}
+  Lemma |*foo*| : forall x : unit, x = tt.
+\end{lstlisting}
+\ssr{} will however accept the $\eta\zeta$ expansion of this rule:
+\begin{lstlisting}
+  Lemma |*fubar*| : forall x : unit, (let u := x in u) = tt.
+\end{lstlisting}
+\item In standard \Coq{}, suppose that we work in the following context:
+\begin{lstlisting}
+  Variable g : nat -> nat.
+  Definition |*f*| := g.
+\end{lstlisting}
+then rewriting \ssrC{H : forall x, f x = 0} in the goal
+\ssrC{g 3 + g 3 = g 6} succeeds
+and transforms the goal into \ssrC{0 + 0 = g 6}.
+
+This rewriting is not possible in \ssr{} because there is no
+occurrence of the head symbol \ssrC{f} of the rewrite rule in the
+goal. Rewriting with \ssrC{H} first requires unfolding the occurrences of
+\ssrC{f} where the substitution is to be performed (here there is a single
+such occurrence), using tactic \ssrC{rewrite /f} (for a global
+replacement of \ssrC{f} by \ssrC{g}) or \ssrC{rewrite $\ \ssrN{pattern}$/f}, for a
+finer selection.
+\end{itemize}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Existential metavariables and rewriting}
+\label{ssec:rewcaveats}
+The \ssrC{rewrite} tactic will not instantiate existing existential
+metavariables when matching a redex pattern.
+
+If a rewrite rule generates a goal
+with new existential metavariables, these will be generalized as for \ssrC{apply}
+(see page~\pageref{sssec:apply}) and corresponding new goals will be generated.
+For example, consider the following script:
+
+\begin{lstlisting}
+  Lemma |*ex3*| (x : 'I_2) y (le_1 : y < 1) (E : val x = y) : Some x = insub y.
+  rewrite insubT ?(leq_trans le_1)// => le_2.
+\end{lstlisting}
+
+Since \ssrC{insubT} has the following type:
+
+\begin{lstlisting}
+  forall T P (sT : subType P) (x : T) (Px : P x), insub x = Some (Sub x Px)
+\end{lstlisting}
+
+and since the implicit argument corresponding to the \ssrC{Px} abstraction is not
+supplied by the user, the resulting goal should be \ssrC{Some x = Some (Sub y
+$\;\;?_{Px}$)}. Instead, \ssr{} \ssrC{rewrite} tactic generates the two following
+goals:
+\begin{lstlisting}
+  y < 2
+  forall Hyp0 : y < 2, Some x = Some (Sub y Hyp0)
+\end{lstlisting}
+The script closes the former with \ssrC{?(leq_trans le_1)//}, then it introduces
+the new generalization naming it \ssrC{le_2}.
+
+\begin{lstlisting}
+  x : 'I_2
+  y : nat
+  le_1 : y < 1
+  E : val x = y
+  le_2 : y < 2
+  ============================
+   Some x = Some (Sub y le_2)
+\end{lstlisting}
+
+As a temporary limitation, this behavior is available only if the rewriting
+rule is stated using Leibniz equality (as opposed to setoid relations).
+It will be extended to other rewriting relations in the future.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Locking, unlocking} \label{ssec:lock}
+
+As program proofs tend to generate large goals, it is important to be
+able to control the partial evaluation performed by the simplification
+operations that are performed by the tactics. These evaluations can
+for example come from a \ssrC{/=} simplification switch, or from rewrite steps
+which may expand large terms while performing conversion. We definitely
+want to avoid repeating large subterms of the goal in
+the proof script. We do this by
+``clamping down'' selected function symbols in the goal, which
+prevents them from
+being considered in simplification or rewriting steps. This clamping
+is accomplished by using the occurrence switches (see section
+\ref{sssec:occselect}) together with ``term tagging'' operations.
+
+\ssr{} provides two levels of tagging.
+
+The first one uses auxiliary definitions to introduce a provably equal
+copy of any term \ssrC{t}. However this copy is (on purpose)
+\emph{not convertible} to \ssrC{t} in the \Coq{} system\footnote{This is
+  an implementation feature: there is not such obstruction in the
+  metatheory}. The job is done by the following construction:
+
+\begin{lstlisting}
+  Lemma |*master_key*| : unit. Proof. exact tt. Qed.
+  Definition |*locked*| A := let: tt := master_key in fun x : A => x.
+  Lemma |*lock*| : forall A x, x = locked x :> A.
+\end{lstlisting}
+Note that the definition of \ssrC{|*master_key*|} is explicitly opaque.
+The equation \ssrC{t = locked t} given by the \ssrC{lock} lemma can be used
+for selective rewriting, blocking on the fly the reduction in the
+term \ssrC{t}.
+For example the script:
+\begin{lstlisting}
+  Require Import List.
+  Variable A : Type.
+
+  Fixpoint |*my_has*| (p : A -> bool)(l : list A){struct l} : bool:=
+    match l with
+      |nil => false
+      |cons x l => p x || (my_has p l)
+    end.
+
+  Goal forall a x y l, a x = true -> my_has a ( x :: y :: l) = true.
+  move=> a x y l Hax.
+\end{lstlisting}
+where \ssrL{||} denotes the boolean disjunction, results in a goal
+\ssrC{my_has a ( x :: y :: l) = true}. The tactic:
+\begin{lstlisting}
+  rewrite {2}[cons]lock /= -lock.
+\end{lstlisting}
+turns it into \ssrC{a x || my_has a (y :: l) = true}.
+Let us now start by reducing the initial goal without blocking reduction.
+The script:
+\begin{lstlisting}
+  Goal forall a x y l, a x = true -> my_has a ( x :: y :: l) = true.
+  move=> a x y l Hax /=.
+\end{lstlisting}
+creates a goal \ssrC{(a x) || (a y) || (my_has a l) = true}. Now the
+tactic:
+\begin{lstlisting}
+  rewrite {1}[orb]lock orbC -lock.
+\end{lstlisting}
+where \ssrC{orbC} states the commutativity of \ssrC{orb}, changes the
+goal into\\ \ssrC{(a x) || (my_has a l) || (a y) = true}: only the
+arguments of the second disjunction where permuted.
+
+
+It is sometimes desirable to globally prevent a definition from being
+expanded by simplification; this is done by adding \ssrC{locked} in the
+definition.
+
+For instance, the function \ssrC{|*fgraph_of_fun*|} maps a function whose
+domain and codomain are finite types to a concrete representation of
+its (finite) graph. Whatever implementation of this transformation we
+may use, we want it to be hidden to simplifications and tactics, to
+avoid the collapse of the graph object:
+\begin{lstlisting}
+  Definition |*fgraph_of_fun*| :=
+    locked
+    (fun (d1 :finType) (d2 :eqType) (f : d1 -> d2) => Fgraph (size_maps f _)).
+\end{lstlisting}
+
+We provide a special tactic \ssrC{unlock} for unfolding such definitions
+while removing ``locks'', e.g., the tactic:
+
+  \ssrC{unlock} \ssrN{occ-switch}\ssrC{fgraph_of_fun}.
+
+replaces the occurrence(s) of \ssrC{fgraph_of_fun} coded by the \ssrN{occ-switch}
+with \ssrC{(Fgraph (size_maps _ _))} in the goal.
+
+We found that it was usually preferable to prevent the expansion of
+some functions by the partial evaluation switch ``/='', unless
+this allowed the evaluation of a condition. This is possible thanks to
+an other mechanism of term tagging, resting on the following
+\emph{Notation}:
+\begin{lstlisting}
+  Notation "'nosimpl' t" := (let: tt := tt in t).
+\end{lstlisting}
+
+The term \ssrC{(nosimpl t)} simplifies to t \emph{except} in a
+definition. More precisely,
+given:
+\begin{lstlisting}
+  Definition |*foo*| := (nosimpl bar).
+\end{lstlisting}
+the term \ssrC{foo (or (foo t'))} will \emph{not} be expanded by the
+\emph{simpl} tactic unless it is in a forcing context (e.g., in
+\ssrC{match foo t' with $\dots$ end}, \ssrC{foo t'} will be reduced if this allows
+\ssrC{match} to be reduced). Note that \ssrC{nosimpl bar} is simply notation
+for a term that reduces to \ssrC{bar}; hence \ssrC{unfold foo} will replace
+    \ssrC{foo} by \ssrC{bar}, and \ssrC{fold foo} will replace \ssrC{bar} by
+    \ssrC{foo}.
+
+\emph{Warning} The \ssrC{nosimpl} trick only works if no reduction is
+apparent in \ssrC{t}; in particular, the declaration:
+\begin{lstlisting}
+  Definition |*foo*| x := nosimpl (bar x).
+\end{lstlisting}
+will usually not work. Anyway, the common practice is to tag only the
+function, and to use the following definition, which blocks the
+reduction as expected:
+\begin{lstlisting}
+  Definition |*foo*| x := nosimpl bar x.
+\end{lstlisting}
+
+
+A standard example making this technique shine is the case of
+arithmetic operations. We define for instance:
+\begin{lstlisting}
+  Definition |*addn*| := nosimpl plus.
+\end{lstlisting}
+The operation \ssrC{addn} behaves exactly like plus, except that
+\ssrC{(addn (S n) m)} will not
+simplify spontaneously to \ssrC{(S (addn n m))} (the two terms, however, are
+inter-convertible). In addition, the unfolding step:
+\begin{lstlisting}
+rewrite /addn
+\end{lstlisting}
+will replace \ssrC{addn} directly with \ssrC{plus}, so the \ssrC{nosimpl} form
+is essentially invisible.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Congruence}\label{ssec:congr}
+
+Because of the way matching interferes with type families parameters,
+the tactic:
+\begin{lstlisting}
+  apply: my_congr_property.
+\end{lstlisting}
+will generally fail to perform congruence simplification, even on
+rather simple cases. We therefore provide a
+more robust alternative in which the function is supplied:
+$$\ssrC{congr}\ [\ssrN{int}]\ {\term}$$
+
+This tactic:
+\begin{itemize}
+\item checks that the goal is a Leibniz equality
+\item matches both sides of this equality with ``{\term} applied to
+  some arguments'', inferring the right number of arguments from the goal
+  and the type of {\term}. This may
+  expand some definitions or fixpoints.
+\item generates the subgoals corresponding to pairwise equalities of
+  the arguments present in the goal.
+\end{itemize}
+
+The goal can be a non dependent product \ssrC{P -> Q}.
+In that case, the system asserts the equation \ssrC{P = Q}, uses it to solve
+the goal, and calls the \ssrC{congr} tactic on the remaining goal
+\ssrC{P = Q}. This can be useful for instance to perform a transitivity
+step, like in the following situation:
+\begin{lstlisting}
+  x, y, z : nat
+  ===============
+  x = y -> x = z
+\end{lstlisting}
+the tactic \ssrC{congr (_ = _)} turns this goal into:
+
+\begin{lstlisting}
+  x, y, z : nat
+  ===============
+  y = z
+\end{lstlisting}
+which can also be obtained starting from:
+\begin{lstlisting}
+  x, y, z : nat
+  h : x = y
+  ===============
+  x = z
+\end{lstlisting}
+and using the tactic \ssrC{congr (_ = _): h}.
+
+The optional \ssrN{int} forces the number of arguments for which the
+tactic should generate equality proof obligations.
+
+This tactic supports equalities between applications with dependent
+arguments. Yet dependent arguments should have exactly the same
+parameters on both sides, and these parameters should appear as first
+arguments.
+
+The following script:
+\begin{lstlisting}
+  Definition f n := match n with 0 => plus | S _ => mult end.
+  Definition g (n m : nat) := plus.
+
+  Goal forall x y, f 0 x y = g 1 1 x y.
+  by move=> x y; congr plus.
+  Qed.
+\end{lstlisting}
+shows that the \ssrC{congr} tactic matches \ssrC{plus} with \ssrC{f 0} on the
+left hand side and \ssrC{g 1 1} on the right hand side, and solves the goal.
+
+The script:
+\begin{lstlisting}
+  Goal forall n m, m <= n -> S m + (S n - S m) = S n.
+  move=> n m Hnm; congr S; rewrite -/plus.
+\end{lstlisting}
+generates the subgoal \ssrC{m + (S n - S m) = n}. The tactic
+\ssrC{rewrite -/plus} folds back the expansion of \ssrC{plus} which was
+necessary for matching both sides of the equality with an application
+of \ssrC{S}.
+
+Like most \ssr{} arguments, {\term} can contain wildcards.
+The script:
+\begin{lstlisting}
+  Goal forall x y, x + (y * (y + x - x)) = x * 1 + (y + 0) * y.
+  move=> x y; congr ( _ + (_ * _)).
+\end{lstlisting}
+generates three subgoals, respectively \ssrC{x = x * 1}, \ssrC{y = y + 0}
+and \ssrC{ y + x - x = y}.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Contextual patterns}
+\label{ssec:rewp}
+
+The simple form of patterns used so far, ${\term}s$ possibly containing
+wild cards, often require an additional \ssrN{occ-switch} to be specified.
+While this may work pretty fine for small goals, the use of polymorphic
+functions and dependent types may lead to an invisible duplication of functions
+arguments. These copies usually end up in types hidden by the implicit
+arguments machinery or by user defined notations.  In these situations
+computing the right occurrence numbers is very tedious because they must be
+counted on the goal as printed after setting the \ssrC{Printing All} flag.
+Moreover the resulting script is not really informative for the reader, since
+it refers to occurrence numbers he cannot easily see.
+
+Contextual patterns mitigate these issues allowing to specify occurrences
+according to the context they occur in.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Syntax}
+
+The following table summarizes the full syntax of
+\ssrN{c-pattern} and the corresponding subterm(s) identified
+by the pattern.
+In the third column we use s.m.r. for
+``the subterms matching the redex'' specified in the second column.
+
+\begin{center}
+%\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.21\textwidth}|>{\arraybackslash}m{0.39\textwidth}}
+\begin{tabular}{llp{10em}}
+\ssrN{c-pattern} & redex & subterms affected \\
+\hline
+{\term} & {\term} & all occurrences of {\term}\\
+\hline
+$\ssrN{ident}\ \ssrC{in}\ {\term}$ &
+  subterm of {\term} selected by \ssrN{ident} &
+  all the subterms identified by \ssrN{ident} in all
+  the occurrences of {\term} \\
+\hline
+$\ssrN[1]{term}\ \ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & $\ssrN[1]{term}$ &
+  in all  s.m.r. in all the subterms identified by \ssrN{ident} in all
+  the occurrences of $\ssrN[2]{term}$ \\
+\hline
+$\ssrN[1]{term}\ \ssrC{as}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ & $\ssrN[1]{term}$ &
+  in all the subterms identified by \ssrN{ident} in all
+  the occurrences of $\ssrN[2]{term}[\ssrN[1]{term}/\ssrN{ident}]$\\
+\hline
+%\end{tabularx}
+\end{tabular}
+\end{center}
+
+The \ssrC{rewrite} tactic supports two more patterns obtained
+prefixing the first two with \ssrC{in}. The intended meaning is that the
+pattern identifies all subterms of the specified context. The
+\ssrC{rewrite} tactic will infer a pattern for the redex looking at the
+rule used for rewriting.
+
+\begin{center}
+\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.21\textwidth}|>{\arraybackslash}m{0.39\textwidth}}
+\ssrN{r-pattern} & redex & subterms affected \\
+\hline
+$\ssrC{in}\ {\term}$ & inferred from rule &
+  in all  s.m.r. in all occurrences of {\term}\\
+\hline
+$\ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ {\term}$ & inferred from rule &
+  in all  s.m.r. in all the subterms identified by \ssrN{ident} in all
+  the occurrences of {\term} \\
+\hline
+\end{tabularx}
+\end{center}
+
+The first \ssrN{c-pattern} is the simplest form matching any
+context but selecting a specific redex and has been described in the
+previous sections. We have seen so far that the possibility of
+selecting a redex using a term with holes is already a powerful mean of redex
+selection. Similarly, any {\term}s provided by the
+user in the more complex forms of \ssrN{c-pattern}s presented in the
+tables above can contain holes.
+
+For a quick glance at what can be expressed with the last
+\ssrN{r-pattern} consider the goal \ssrC{a = b} and the tactic
+\begin{lstlisting}
+  rewrite [in X in _ = X]rule.
+\end{lstlisting}
+It rewrites all occurrences of the left hand side of \ssrC{rule} inside
+\ssrC{b} only (\ssrC{a}, and the hidden type of the equality, are ignored).
+Note that the variant \ssrC{rewrite [X in _ = X]rule} would have
+rewritten \ssrC{b} exactly (i.e., it would only work if \ssrC{b} and the
+left hand side of \ssrC{rule} can be unified).
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Matching contextual patterns}
+
+The \ssrN{c-pattern}s and \ssrN{r-pattern}s involving
+{\term}s with holes are matched
+against the goal in order to find a closed instantiation. This
+matching proceeds as follows:
+
+\begin{center}
+\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.65\textwidth}}
+\ssrN{c-pattern} & instantiation order and place for $\ssrN[i]{term}$ and redex\\
+\hline
+{\term} & {\term} is matched against the goal, redex is unified with
+    the instantiation of {\term}\\
+\hline
+$\ssrN{ident}\ \ssrC{in}\ {\term}$ &
+    {\term} is matched against the goal, redex is
+    unified with the subterm of the
+    instantiation of {\term} identified by \ssrN{ident}\\
+\hline
+$\ssrN[1]{term}\ \ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ &
+    $\ssrN[2]{term}$ is matched against the goal, $\ssrN[1]{term}$ is
+    matched against the subterm of the
+    instantiation of $\ssrN[1]{term}$ identified by \ssrN{ident},
+    redex is unified with the instantiation of $\ssrN[1]{term}$\\
+\hline
+$\ssrN[1]{term}\ \ssrC{as}\ \ssrN{ident}\ \ssrC{in}\ \ssrN[2]{term}$ &
+    $\ssrN[2]{term}[\ssrN[1]{term}/\ssrN{ident}]$
+    is matched against the goal,
+    redex is unified with the instantiation of $\ssrN[1]{term}$\\
+\hline
+\end{tabularx}
+\end{center}
+
+In the following patterns, the redex is intended to be inferred from the
+rewrite rule.
+
+\begin{center}
+\begin{tabularx}{\textwidth}{>{\arraybackslash}m{0.30\textwidth}|>{\arraybackslash}m{0.65\textwidth}}
+\ssrN{r-pattern} & instantiation order and place for $\ssrN[i]{term}$ and redex\\
+\hline
+$\ssrC{in}\ \ssrN{ident}\ \ssrC{in}\ {\term}$ &
+    {\term} is matched against the goal, the redex is
+    matched against the subterm of the
+    instantiation of {\term} identified by \ssrN{ident}\\
+\hline
+$\ssrC{in}\ {\term}$ & {\term} is matched against the goal, redex is
+   matched against the instantiation of {\term}\\
+\hline
+\end{tabularx}
+\end{center}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Examples}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection{Contextual pattern in \ssrC{set} and the \ssrC{:} tactical}
+
+As already mentioned in section~\ref{ssec:set} the \ssrC{set} tactic
+takes as an argument a term in open syntax. This term is interpreted
+as the simplest for of \ssrN{c-pattern}. To void confusion in the grammar,
+open syntax is supported only for the simplest form of patterns, while
+ parentheses are required around more complex patterns.
+
+\begin{lstlisting}
+set t := (X in _ = X).
+set t := (a + _ in X in _ = X).
+\end{lstlisting}
+
+Given the goal \ssrC{a + b + 1 = b + (a + 1)} the first tactic
+captures \ssrC{b + (a + 1)}, while the latter \ssrC{a + 1}.
+
+Since the user may define an infix notation for \ssrC{in} the former
+tactic may result ambiguous. The disambiguation rule implemented is
+to prefer patterns over simple terms, but to interpret a pattern with
+double parentheses as a simple term. For example
+the following tactic would capture any occurrence of the term `\ssrC{a in A}'.
+
+\begin{lstlisting}
+set t := ((a in A)).
+\end{lstlisting}
+
+Contextual pattern can also be used as arguments of the \ssrC{:} tactical.
+For example:
+\begin{lstlisting}
+elim: n (n in _ = n) (refl_equal n).
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection{Contextual patterns in \ssrC{rewrite}}
+As a more comprehensive example consider the following goal:
+\begin{lstlisting}
+    (x.+1 + y) + f (x.+1 + y) (z + (x + y).+1) = 0
+\end{lstlisting}
+The tactic \ssrC{rewrite [in f _ _]addSn} turns it into:
+\begin{lstlisting}
+    (x.+1 + y) + f (x + y).+1 (z + (x + y).+1) = 0
+\end{lstlisting}
+since the simplification rule \ssrC{addSn} is applied only under the \ssrC{f} symbol.
+Then we simplify also the first addition and expand \ssrC{0} into \ssrC{0+0}.
+\begin{lstlisting}
+    rewrite addSn -[X in _ = X]addn0.
+\end{lstlisting}
+obtaining:
+\begin{lstlisting}
+    (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + 0
+\end{lstlisting}
+Note that the right hand side of \ssrC{addn0} is undetermined, but the
+rewrite pattern specifies the redex explicitly. The right hand side of
+\ssrC{addn0} is unified with the term identified by \ssrC{X}, \ssrC{0} here.
+
+The following pattern does not specify a redex, since it
+identifies an entire region, hence the rewrite rule has to be instantiated
+explicitly. Thus the tactic:
+\begin{lstlisting}
+    rewrite -{2}[in X in _ = X](addn0 0).
+\end{lstlisting}
+changes the goal as follows:
+\begin{lstlisting}
+    (x + y).+1 + f (x + y).+1 (z + (x + y).+1) = 0 + (0 + 0)
+\end{lstlisting}
+The following tactic is quite tricky:
+\begin{lstlisting}
+    rewrite [_.+1 in X in f _ X](addnC x.+1).
+\end{lstlisting}
+and the resulting goals is:
+\begin{lstlisting}
+    (x + y).+1 + f (x + y).+1 (z + (y + x.+1)) = 0 + (0 + 0)
+\end{lstlisting}
+The explicit redex \ssrC{_.+1} is important since its head
+constant \ssrC{S} differs from the head constant inferred from
+\ssrC{(addnC x.+1)} (that is \ssrC{addn}, denoted \ssrC{+} here).
+Moreover, the pattern \ssrC{f _ X} is important to rule out the first occurrence
+of \ssrC{(x + y).+1}. Last, only the subterms of \ssrC{f _ X} identified by \ssrC{X} are
+rewritten, thus the first argument of \ssrC{f} is skipped too.
+Also note the pattern \ssrC{_.+1} is interpreted in the context
+identified by \ssrC{X}, thus it gets instantiated to \ssrC{(y + x).+1} and
+not \ssrC{(x + y).+1}.
+
+The last rewrite pattern allows to specify exactly the shape of the term
+identified by \ssrC{X}, that is thus unified with the left hand side of the
+rewrite rule.
+\begin{lstlisting}
+    rewrite [x.+1 + y as X in f X _]addnC.
+\end{lstlisting}
+The resulting goal is:
+\begin{lstlisting}
+    (x + y).+1 + f (y + x.+1) (z + (y + x.+1)) = 0 + (0 + 0)
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Patterns for recurrent contexts}
+
+The user can define shortcuts for recurrent contexts corresponding to the
+\ssrN{ident} \ssrC{in} {\term} part. The notation scope identified
+with \ssrC{\%pattern} provides a special notation `\ssrC{(X in t)}' the user
+must adopt to define context shortcuts.
+
+The following example is taken from \ssrC{ssreflect.v} where the
+\ssrC{LHS} and \ssrC{RHS} shortcuts are defined.
+
+\begin{lstlisting}
+Notation RHS := (X in _ = X)%pattern.
+Notation LHS := (X in X = _)%pattern.
+\end{lstlisting}
+
+Shortcuts defined this way can be freely used in place of the
+trailing \ssrN{ident} \ssrC{in} {\term} part of any contextual
+pattern.
+Some examples follow:
+
+\begin{lstlisting}
+set rhs := RHS.
+rewrite [in RHS]rule.
+case: (a + _ in RHS).
+\end{lstlisting}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Views and reflection}\label{sec:views}
+
+The bookkeeping facilities presented in section \ref{sec:book} are
+crafted to ease simultaneous introductions and generalizations of facts and
+casing,
+naming $\dots$ operations. It also a common practice to make a stack
+operation immediately followed by an \emph{interpretation} of the fact
+being pushed,
+that is, to apply a lemma to this fact before passing it
+to a tactic for decomposition, application and so on.
+
+
+% possibly
+
+% Small scale reflection consists in using a two levels
+% approach locally when developing formal proofs. This means that a
+% fact, which may be an assumption, or the goal itself, will often be
+% \emph{interpreted} before being passed to a tactic
+% for decomposition, application and so on.
+
+\ssr{} provides a convenient, unified syntax to combine these
+interpretation operations with the proof stack operations. This
+\emph{view mechanism} relies on the combination of the \ssrC{/} view
+switch with bookkeeping tactics and tacticals.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Interpreting eliminations}
+\idx{elim/\dots{}}
+
+The view syntax combined with the \ssrC{elim} tactic specifies an
+elimination scheme to
+be used instead of the default, generated, one. Hence the \ssr{} tactic:
+\begin{lstlisting}
+  elim/V.
+\end{lstlisting}
+is a synonym for:
+\begin{lstlisting}
+  intro top; elim top using V; clear top.
+\end{lstlisting}
+where \ssrC{top} is a fresh name and \ssrC{V} any second-order lemma.
+
+Since an elimination view supports the two bookkeeping tacticals of
+discharge and introduction (see section \ref{sec:book}), the \ssr{} tactic:
+\begin{lstlisting}
+  elim/V: x => y.
+\end{lstlisting}
+is a synonym for:
+\begin{lstlisting}
+  elim x using V; clear x; intro y.
+\end{lstlisting}
+where \ssrC{x} is a variable in the context, \ssrC{y} a fresh name and \ssrC{V}
+any second order lemma; \ssr{} relaxes the syntactic restrictions of
+the \Coq{} \ssrC{elim}. The first pattern following \ssrC{:} can be a \ssrC{_}
+wildcard if the conclusion of the view \ssrC{V} specifies a pattern for
+its last argument (e.g., if \ssrC{V} is a functional induction lemma
+generated by the \ssrC{Function} command).
+
+The elimination view mechanism is compatible with the equation name
+generation (see section \ref{ssec:equations}).
+
+The following script illustrate a toy example of this feature. Let us
+define a function adding an element at the end of a list:
+\begin{lstlisting}
+  Require Import List.
+
+  Variable d : Type.
+
+  Fixpoint |*add_last*|(s : list d) (z : d) {struct s} : list d :=
+    match s with
+    | nil =>  z :: nil
+    | cons x s' => cons x (add_last s' z)
+    end.
+\end{lstlisting}
+
+One can define an alternative, reversed, induction principle on inductively
+defined \ssrC{list}s, by proving the following lemma:
+
+\begin{lstlisting}
+  Lemma |*last_ind_list*| : forall (P : list d -> Type),
+  P nil ->
+  (forall (s : list d) (x : d), P s -> P (add_last s x)) -> forall s : list d, P s.
+\end{lstlisting}
+
+Then the combination of elimination views with equation names result
+in a concise syntax for reasoning inductively using the user
+defined elimination scheme. The script:
+\begin{lstlisting}
+  Goal forall (x : d)(l : list d), l = l.
+  move=> x l.
+  elim/last_ind_list E : l=> [| u v]; last first.
+\end{lstlisting}
+generates two subgoals: the first one to prove \ssrC{nil = nil} in a
+context featuring \ssrC{E : l = nil} and the second to prove
+\ssrC{add_last u v = add_last u v}, in a context containing
+\ssrC{E : l = add_last u v}.
+
+User provided eliminators (potentially generated with the
+\ssrC{Function} \Coq{}'s command) can be combined with the type family switches
+described in section~\ref{ssec:typefam}. Consider an eliminator
+\ssrC{foo_ind} of type:
+
+  \ssrC{foo_ind : forall $\dots$, forall x : T, P p$_1$ $\dots$ p$_m$}
+
+and consider the tactic
+
+  \ssrC{elim/foo_ind: e$_1$ $\dots$ / e$_n$}
+
+The \ssrC{elim/} tactic distinguishes two cases:
+\begin{description}
+\item[truncated eliminator] when \ssrC{x} does not occur in \ssrC{P p$_1 \dots$ p$_m$}
+  and the type of \ssrC{e$_n$} unifies with \ssrC{T} and \ssrC{e$_n$} is not \ssrC{_}.
+  In that case, \ssrC{e$_n$} is passed to the eliminator as the last argument
+  (\ssrC{x} in \ssrC{foo_ind}) and \ssrC{e$_{n-1} \dots$ e$_1$} are used as patterns
+  to select in the goal the occurrences that will be bound by the
+  predicate \ssrC{P}, thus it must be possible to unify the sub-term of
+  the goal matched by \ssrC{e$_{n-1}$} with \ssrC{p$_m$}, the one matched by
+  \ssrC{e$_{n-2}$} with \ssrC{p$_{m-1}$} and so on.
+\item[regular eliminator] in all the other cases. Here it must be
+  possible to unify the term matched by
+  \ssrC{e$_n$} with \ssrC{p$_m$}, the one matched by
+  \ssrC{e$_{n-1}$} with \ssrC{p$_{m-1}$} and so on. Note that
+  standard eliminators have the shape \ssrC{$\dots$forall x, P $\dots$ x}, thus
+  \ssrC{e$_n$} is the pattern identifying the eliminated term, as expected.
+\end{description}
+As explained in  section~\ref{ssec:typefam}, the initial prefix of
+\ssrC{e$_i$} can be omitted.
+
+Here an example of a regular, but non trivial, eliminator:
+\begin{lstlisting}
+  Function |*plus*| (m n : nat) {struct n} : nat :=
+     match n with 0 => m | S p => S (plus m p) end.
+\end{lstlisting}
+The type of \ssrC{plus_ind} is
+\begin{lstlisting}
+plus_ind : forall (m : nat) (P : nat -> nat -> Prop),
+  (forall n : nat, n = 0 -> P 0 m) ->
+  (forall n p : nat, n = p.+1 -> P p (plus m p) -> P p.+1 (plus m p).+1) ->
+    forall n : nat, P n (plus m n)
+\end{lstlisting}
+Consider the following goal
+\begin{lstlisting}
+  Lemma |*exF*| x y z: plus (plus x y) z = plus x (plus y z).
+\end{lstlisting}
+The following tactics are all valid and perform the same elimination
+on that goal.
+\begin{lstlisting}
+  elim/plus_ind: z / (plus _ z).
+  elim/plus_ind: {z}(plus _ z).
+  elim/plus_ind: {z}_.
+  elim/plus_ind: z / _.
+\end{lstlisting}
+In the two latter examples, being the user provided pattern a wildcard, the
+pattern inferred from the type of the eliminator is used instead.  For both
+cases it is \ssrC{(plus _ _)} and matches the subterm \ssrC{plus (plus x y)$\;$z} thus
+instantiating the latter \ssrC{_} with \ssrC{z}.  Note that the tactic
+\ssrC{elim/plus_ind: y / _} would have resulted in an error, since \ssrC{y} and \ssrC{z}
+do no unify but the type of the eliminator requires the second argument of
+\ssrC{P} to be the same as the second argument of \ssrC{plus} in the second
+argument of \ssrC{P}.
+
+Here an example of a truncated eliminator. Consider the goal
+\begin{lstlisting}
+  p : nat_eqType
+  n : nat
+  n_gt0 : 0 < n
+  pr_p : prime p
+ =================
+  p %| \prod_(i <- prime_decomp n | i \in prime_decomp n) i.1 ^ i.2 ->
+    exists2 x : nat * nat, x \in prime_decomp n & p = x.1
+\end{lstlisting}
+and the tactic
+\begin{lstlisting}
+elim/big_prop: _ => [| u v IHu IHv | [q e] /=].
+\end{lstlisting}
+where the type of the eliminator is
+\begin{lstlisting}
+big_prop: forall (R : Type) (Pb : R -> Type) (idx : R) (op1 : R -> R -> R),
+  Pb idx ->
+  (forall x y : R, Pb x -> Pb y -> Pb (op1 x y)) ->
+  forall (I : Type) (r : seq I) (P : pred I) (F : I -> R),
+  (forall i : I, P i -> Pb (F i)) ->
+    Pb (\big[op1/idx]_(i <- r | P i) F i)
+\end{lstlisting}
+Since the pattern for the argument of \ssrC{Pb} is not specified, the inferred one
+is used instead: \ssrC{(\\big[_/_]_(i <- _ | _ i) _ i)}, and after the
+introductions, the following goals are generated.
+\begin{lstlisting}
+subgoal 1 is:
+ p %| 1 -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1
+subgoal 2 is:
+ p %| u * v -> exists2 x : nat * nat, x \in prime_decomp n & p = x.1
+subgoal 3 is:
+ (q, e) \in prime_decomp n -> p %| q ^ e ->
+   exists2 x : nat * nat, x \in prime_decomp n & p = x.1
+\end{lstlisting}
+Note that the pattern matching algorithm instantiated all the variables
+occurring in the pattern.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Interpreting assumptions}\label{ssec:assumpinterp}
+\idx{move/\dots{}}
+
+Interpreting an assumption in the context of a proof is applying it a
+correspondence lemma before generalizing, and/or decomposing it.
+For instance, with the extensive use of boolean reflection (see
+section \ref{ssec:boolrefl}), it is
+quite frequent to need to decompose the logical interpretation of (the
+boolean expression of) a
+fact, rather than the fact itself.
+This can be achieved by a combination of \ssrC{move : _ => _}
+switches, like in the following script, where \ssrC{||} is a notation for
+the boolean disjunction:
+\begin{lstlisting}
+  Variables P Q : bool -> Prop.
+  Hypothesis |*P2Q*| : forall a b, P (a || b) -> Q a.
+
+  Goal forall a, P (a || a) -> True.
+  move=> a HPa; move: {HPa}(P2Q _ _ HPa) => HQa.
+\end{lstlisting}
+which transforms the hypothesis \ssrC{HPn : P n} which has been
+introduced from the initial statement into \ssrC{HQn : Q n}.
+This operation is so common that the tactic shell has
+specific syntax for it.
+The following scripts:
+\begin{lstlisting}
+  Goal forall a, P (a || a) -> True.
+  move=> a HPa; move/P2Q: HPa => HQa.
+\end{lstlisting}
+or more directly:
+\begin{lstlisting}
+  Goal forall a, P (a || a) -> True.
+  move=> a; move/P2Q=> HQa.
+\end{lstlisting}
+are equivalent to the former one. The former script shows how to
+interpret a fact (already in the context), thanks to the discharge
+tactical (see section \ref{ssec:discharge}) and the latter, how to
+interpret the top assumption of a goal. Note
+that the number of wildcards to be inserted to find the correct
+application of the view lemma to the hypothesis has been automatically
+inferred.
+
+The view mechanism is compatible with the \ssrC{case} tactic and with the
+equation name generation mechanism (see section \ref{ssec:equations}):
+\begin{lstlisting}
+  Variables P Q: bool -> Prop.
+  Hypothesis |*Q2P*| : forall a b, Q (a || b) -> P a \/ P b.
+
+  Goal forall a b, Q (a || b) -> True.
+  move=> a b; case/Q2P=> [HPa | HPb].
+\end{lstlisting}
+creates two new subgoals whose contexts no more contain
+\ssrC{HQ : Q (a || b)} but respectively \ssrC{HPa : P a} and
+\ssrC{HPb : P b}. This view tactic
+performs:
+\begin{lstlisting}
+  move=> a b HQ; case: {HQ}(Q2P _ _ HQ) => [HPa | HPb].
+\end{lstlisting}
+
+The term on the right of the \ssrC{/} view switch is called a \emph{view
+  lemma}. Any \ssr{} term coercing to a product type can be used as a
+view lemma.
+
+
+The examples we have given so far explicitly provide the direction of the
+translation to be performed. In fact, view lemmas need not to be
+oriented. The view mechanism is able to detect which
+application is relevant for the current goal. For instance, the
+script:
+\begin{lstlisting}
+  Variables P Q: bool -> Prop.
+  Hypothesis |*PQequiv*| : forall a b, P (a || b) <-> Q a.
+
+  Goal forall a b, P (a || b) -> True.
+  move=> a b; move/PQequiv=> HQab.
+\end{lstlisting}
+has the same behavior as the first example above.
+
+The view mechanism can insert automatically a \emph{view hint} to
+transform the double implication into the expected simple implication.
+The last script is in fact equivalent to:
+\begin{lstlisting}
+  Goal forall a b, P (a || b) -> True.
+  move=> a b; move/(iffLR (PQequiv _ _)).
+\end{lstlisting}
+where:
+\begin{lstlisting}
+  Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q.
+\end{lstlisting}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Specializing assumptions}
+\idx{move/\dots{}}
+
+The special case when the \emph{head symbol} of the view lemma is a
+wildcard is used to interpret an assumption by \emph{specializing}
+it. The view mechanism hence offers the possibility to
+apply a higher-order assumption to some given arguments.
+
+For example, the script:
+\begin{lstlisting}
+  Goal forall z, (forall x y, x + y = z -> z = x) -> z = 0.
+  move=> z; move/(_ 0 z).
+\end{lstlisting}
+changes the goal into:
+\begin{lstlisting}
+  (0 + z = z -> z = 0) -> z = 0
+\end{lstlisting}
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Interpreting goals}\label{ssec:goalinterp}
+
+In a similar way, it is also often convenient to interpret a goal by changing
+it into an equivalent proposition. The view mechanism of \ssr{} has a
+special syntax \ssrC{apply/} for combining simultaneous goal
+interpretation operations and
+bookkeeping steps in a single tactic.
+
+With the hypotheses of section \ref{ssec:assumpinterp}, the following
+script, where \ssrL+~~+ denotes the boolean negation:
+\begin{lstlisting}
+  Goal forall a, P ((~~ a) || a).
+  move=> a; apply/PQequiv.
+\end{lstlisting}
+transforms the goal into \ssrC{Q (~~ a)}, and is equivalent to:
+\begin{lstlisting}
+  Goal forall a, P ((~~ a) || a).
+  move=> a; apply: (iffRL (PQequiv _ _)).
+\end{lstlisting}
+where \ssrC{iffLR} is the analogous of \ssrC{iffRL} for the converse
+implication.
+
+Any \ssr{} term whose type coerces to a double implication can be used
+as a view for goal interpretation.
+
+Note that the goal interpretation view mechanism supports both
+\ssrC{apply} and \ssrC{exact} tactics. As expected, a goal interpretation
+view command \ssrC{exact/$term$} should solve the current goal or it will
+fail.
+
+
+\emph{Warning} Goal interpretation view tactics are \emph{not} compatible
+with the bookkeeping tactical \ssrC{=>} since this would be redundant with
+the \ssrC{apply:} {\term} \ssrC{=> _} construction.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Boolean reflection}\label{ssec:boolrefl}
+In the Calculus of Inductive Construction, there is
+an obvious distinction between logical propositions and boolean values.
+On the one hand, logical propositions are objects
+of \emph{sort} \ssrC{Prop} which is the carrier of intuitionistic
+reasoning. Logical connectives in \ssrC{Prop} are \emph{types}, which give precise
+information on the structure of their proofs; this information is
+automatically exploited by \Coq{} tactics. For example, \Coq{} knows that a
+proof of \ssrL+A \/ B+ is either a proof of \ssrC{A} or a proof of \ssrC{B}.
+The tactics \ssrC{left} and \ssrC{right} change the goal \ssrL+A \/ B+
+to \ssrC{A} and \ssrC{B}, respectively; dualy, the tactic \ssrC{case} reduces the goal
+\ssrL+A \/ B => G+ to two subgoals \ssrC{A => G} and \ssrC{B => G}.
+
+On the other hand, \ssrC{bool} is an inductive \emph{datatype}
+with two constructors \ssrC{true} and \ssrC{false}.
+Logical connectives on \ssrC{bool} are \emph{computable functions}, defined by
+their truth tables, using case analysis:
+\begin{lstlisting}
+  Definition (b1 || b2) := if b1 then true else b2.
+\end{lstlisting}
+Properties of such connectives are also established using case
+analysis: the tactic \ssrC{by case: b} solves the goal
+\begin{lstlisting}
+  b || ~~ b = true
+\end{lstlisting}
+by replacing \ssrC{b} first by \ssrC{true} and then by \ssrC{false}; in either case,
+the resulting subgoal reduces by computation to the trivial
+\ssrC{true = true}.
+
+Thus, \ssrC{Prop} and \ssrC{bool} are truly complementary: the former
+supports robust natural deduction, the latter allows brute-force
+evaluation.
+\ssr{} supplies
+a generic mechanism to have the best of the two worlds and move freely
+from a propositional version of a
+decidable predicate to its boolean version.
+
+First, booleans are injected into propositions
+using the coercion mechanism:
+\begin{lstlisting}
+  Coercion |*is_true*| (b : bool) := b = true.
+\end{lstlisting}
+This allows any boolean formula~\ssrC{b} to be used in a context
+where \Coq{} would expect a proposition, e.g., after \ssrC{Lemma $\dots$ : }.
+It is then interpreted as \ssrC{(is_true b)}, i.e.,
+the  proposition \ssrC{b = true}. Coercions are elided by the pretty-printer,
+so they are essentially transparent to the user.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{The \ssrC{reflect} predicate}\label{ssec:reflpred}
+
+To get all the benefits of the boolean reflection, it is in fact
+convenient to introduce the following inductive predicate
+\ssrC{reflect} to relate propositions and booleans:
+
+\begin{lstlisting}
+  Inductive |*reflect*| (P: Prop): bool -> Type :=
+    | Reflect_true: P => reflect P true
+    | Reflect_false: ~P => reflect P false.
+\end{lstlisting}
+
+The statement \ssrC{(reflect P b)} asserts that \ssrC{(is_true b)}
+and \ssrC{P} are logically equivalent propositions.
+
+For instance, the following lemma:
+\begin{lstlisting}
+  Lemma |*andP*|: forall b1 b2, reflect (b1 /\ b2) (b1 && b2).
+\end{lstlisting}
+relates the boolean conjunction \ssrC{&&} to
+the logical one \ssrL+/\+.
+Note that in \ssrC{andP}, \ssrC{b1} and \ssrC{b2} are two boolean variables and
+the proposition \ssrL+b1 /\ b2+ hides two coercions.
+The conjunction of \ssrC{b1} and \ssrC{b2} can then be viewed
+as \ssrL+b1 /\ b2+  or as \ssrC{b1 && b2}.
+
+
+Expressing logical equivalences through this family of inductive types
+makes possible to take benefit from \emph{rewritable equations}
+associated to the case analysis of \Coq{}'s inductive types.
+
+Since the equivalence predicate is defined in \Coq{} as:
+\begin{lstlisting}
+  Definition |*iff*| (A B:Prop) := (A -> B) /\ (B -> A).
+\end{lstlisting}
+where \ssrC{/\\} is a notation for \ssrC{and}:
+\begin{lstlisting}
+  Inductive |*and*| (A B:Prop) : Prop :=
+    conj : A -> B -> and A B
+\end{lstlisting}
+
+This make case analysis very different according to the way an
+equivalence property has been defined.
+
+
+For instance, if we have proved the lemma:
+\begin{lstlisting}
+  Lemma |*andE*|: forall b1 b2, (b1 /\ b2) <-> (b1 && b2).
+\end{lstlisting}
+let us compare the respective behaviours of \ssrC{andE} and \ssrC{andP} on a
+goal:
+\begin{lstlisting}
+  Goal forall b1 b2, if (b1 && b2) then b1 else ~~(b1||b2).
+\end{lstlisting}
+
+The command:
+\begin{lstlisting}
+  move=> b1 b2; case (@andE b1 b2).
+\end{lstlisting}
+generates a single subgoal:
+\begin{lstlisting}
+  (b1 && b2 -> b1 /\ b2) -> (b1 /\ b2 -> b1 && b2) ->
+                   if b1 && b2 then b1 else ~~ (b1 || b2)
+\end{lstlisting}
+
+while the command:
+\begin{lstlisting}
+  move=> b1 b2; case (@andP b1 b2).
+\end{lstlisting}
+generates two subgoals, respectively \ssrL+b1 /\ b2 -> b1+ and
+\ssrL+~ (b1 /\ b2) -> ~~ (b1 || b2)+.
+
+
+
+Expressing reflection relation through the \ssrC{reflect} predicate
+is hence a very convenient way to deal with classical reasoning, by
+case analysis. Using the \ssrC{reflect} predicate allows moreover to
+program rich specifications inside
+its two constructors, which will be automatically taken into account
+during destruction. This formalisation style gives far more
+efficient specifications than quantified (double) implications.
+
+
+A naming convention in \ssr{} is to postfix the name of view lemmas with \ssrC{P}.
+For example, \ssrC{orP} relates  \ssrC{||} and \ssrL+\/+, \ssrC{negP} relates
+\ssrL+~~+ and \ssrL+~+.
+
+The view mechanism is compatible with \ssrC{reflect} predicates.
+
+For example, the script
+\begin{lstlisting}
+  Goal forall a b : bool, a -> b -> a /\\ b.
+  move=> a b Ha Hb; apply/andP.
+\end{lstlisting}
+changes the goal \ssrL+a /\ b+ to \ssrC{a && b} (see section \ref{ssec:goalinterp}).
+
+Conversely, the script
+\begin{lstlisting}
+  Goal forall a b : bool, a /\ b -> a.
+  move=> a b; move/andP.
+\end{lstlisting}
+changes the goal \ssrL+a /\ b -> a+ into \ssrC{a && b -> a} (see section
+\ref{ssec:assumpinterp}).
+
+
+The same tactics can also be used to perform the converse
+operation, changing a boolean conjunction into a logical one. The view
+mechanism guesses the direction of the
+transformation to be used i.e., the constructor of the \ssrC{reflect}
+predicate which should be chosen.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{General mechanism for interpreting goals and assumptions}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Specializing assumptions}
+\idx{move/\dots{}}
+
+The \ssr{}
+tactic:
+
+  \ssrC{move/(_} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{)}
+
+\noindent
+is equivalent to the tactic:
+
+  \ssrC{intro top; generalize (top} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{); clear top.}
+
+\noindent
+where \ssrC{top} is a fresh name for introducing the top assumption of
+the current goal.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Interpreting assumptions}
+\label{sssec:hypview}
+The general form of an assumption view tactic is:
+
+\begin{center}
+ \optional{\ssrC{move} {\optsep} \ssrC{case}} \ssrC{/} \ssrN[0]{term}
+\end{center}
+
+The term \ssrN[0]{term}, called the \emph{view lemma} can be:
+\begin{itemize}
+\item a (term coercible to a) function;
+\item a (possibly quantified) implication;
+\item a (possibly quantified) double implication;
+\item a (possibly quantified) instance of the \ssrC{reflect} predicate
+  (see section \ref{ssec:reflpred}).
+\end{itemize}
+
+Let \ssrC{top} be the top assumption in the goal.
+
+There are three steps in the behaviour of an assumption view tactic:
+\begin{itemize}
+\item It first introduces \ssrL+top+.
+\item If the type of \ssrN[0]{term} is neither a double implication nor
+  an instance of the \ssrC{reflect} predicate, then the tactic
+  automatically generalises a term of the form:
+  
+\begin{center}
+  \ssrC{(}\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term}\ssrC{)}
+\end{center}
+  
+  where the terms \ssrN[1]{term} $\dots$ \ssrN[n]{term} instantiate the
+  possible quantified variables of \ssrN[0]{term}, in order for
+  \ssrC{(}\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term} \ssrC{top)} to be well typed.
+\item If the type of $\ssrN[0]{term}$ is an equivalence, or
+  an instance of the \ssrC{reflect} predicate, it generalises a term of
+  the form:
+  \begin{center}
+  (\ssrN[vh]{term} (\ssrN[0]{term} \ssrN[1]{term} $\dots$ \ssrN[n]{term}))
+  \end{center}
+  where the term \ssrN[vh]{term} inserted is called an
+  \emph{assumption interpretation view hint}.
+\item It finally clears \ssrC{top}.
+\end{itemize}
+For a \ssrC{case/}\ssrN[0]{term} tactic, the generalisation step is
+replaced by a case analysis step.
+
+\emph{View hints} are declared by the user (see section
+\ref{ssec:vhints}) and are stored in the \ssrC{Hint View} database.
+The proof engine automatically
+detects from the shape of the top assumption \ssrC{top} and of the view
+lemma $\ssrN[0]{term}$ provided to the tactic the appropriate view hint in
+the database to be inserted.
+
+If $\ssrN[0]{term}$ is a double implication, then the view hint \ssrC{A} will
+be one of the defined view hints for implication. These hints are by
+default the ones present in the file {\tt ssreflect.v}:
+\begin{lstlisting}
+  Lemma |*iffLR*| : forall P Q, (P <-> Q) -> P -> Q.
+\end{lstlisting}
+which transforms a double  implication into the left-to-right one, or:
+\begin{lstlisting}
+  Lemma |*iffRL*| : forall P Q, (P <-> Q) -> Q -> P.
+\end{lstlisting}
+which produces the converse implication. In both cases, the two first
+\ssrC{Prop} arguments are implicit.
+
+If $\ssrN[0]{term}$ is an instance of the \ssrC{reflect} predicate, then \ssrC{A}
+will be one of the defined view hints  for the \ssrC{reflect}
+predicate,  which are by
+default the ones present in the file {\tt ssrbool.v}.
+These hints are not only used for choosing the appropriate direction of
+the translation, but they also allow complex transformation, involving
+negations.
+ For instance the hint:
+\begin{lstlisting}
+  Lemma |*introN*| : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~ b.
+\end{lstlisting}
+makes the following script:
+\begin{lstlisting}
+  Goal forall a b : bool, a -> b -> ~~ (a && b).
+  move=> a b Ha Hb. apply/andP.
+\end{lstlisting}
+transforms the goal into \ssrC{ \~ (a /\ b)}.
+In fact\footnote{The current state of the proof shall be displayed by
+  the \ssrC{Show Proof} command of \Coq{} proof mode.}
+this last script does not exactly use the hint \ssrC{introN}, but the
+more general hint:
+\begin{lstlisting}
+  Lemma |*introNTF*| : forall (P : Prop) (b c : bool),
+      reflect P b -> (if c then ~ P else P) -> ~~ b = c
+\end{lstlisting}
+The lemma \ssrL+|*introN*|+ is an instantiation of \ssrC{introNF} using
+ \ssrC{c := true}.
+
+Note that views, being part of \ssrN{i-pattern}, can be used to interpret
+assertions too. For example the following script asserts \ssrC{a \&\& b}
+but actually used its propositional interpretation.
+\begin{lstlisting}
+  Lemma |*test*| (a b : bool) (pab : b && a) : b.
+  have /andP [pa ->] : (a && b) by rewrite andbC.
+\end{lstlisting}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsubsection*{Interpreting goals}
+\idx{apply/\dots{}}
+
+A goal interpretation view tactic of the form:
+
+\begin{center}
+	\ssrC{apply/} \ssrN[0]{term}
+\end{center}
+applied to a goal \ssrC{top} is interpreted in the following way:
+\begin{itemize}
+\item If the type of $\ssrN[0]{term}$ is not an instance of the
+  \ssrC{reflect} predicate, nor an equivalence,
+  then the term $\ssrN[0]{term}$ is applied to the current goal \ssrC{top},
+  possibly inserting implicit arguments.
+\item If the type of $\ssrN[0]{term}$ is an instance of the \ssrC{reflect}
+  predicate or an equivalence, then
+a \emph{goal interpretation view hint} can possibly be inserted, which
+corresponds to the application of a term
+\ssrC{($\ssrN[vh]{term}$ ($\ssrN[0]{term}$ _ $\dots$ _))} to the current
+goal, possibly inserting implicit arguments.
+\end{itemize}
+
+Like assumption interpretation view hints, goal interpretation ones
+are user defined lemmas stored (see section \ref{ssec:vhints}) in the
+\ssrC{Hint View} database bridging
+the possible gap between the type of $\ssrN[0]{term}$ and the type of the
+goal.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Interpreting equivalences}
+\idx{apply/\dots{}/\dots{}}
+
+Equivalent boolean propositions are simply \emph{equal} boolean terms.
+A special construction helps the user to prove boolean equalities by
+considering them as logical double implications (between their coerced
+versions), while
+performing at the same time logical operations on both sides.
+
+The syntax of double views is:
+\begin{center}
+ \ssrC{apply/} \ssrN[l]{term} \ssrC{/} \ssrN[r]{term}
+\end{center}
+
+The term \ssrN[l]{term} is the view lemma applied to the left hand side of the
+equality, \ssrN[r]{term} is the one applied to the right hand side.
+
+In this context, the identity view:
+\begin{lstlisting}
+Lemma |*idP*| : reflect b1 b1.
+\end{lstlisting}
+is useful, for example the tactic:
+\begin{lstlisting}
+  apply/idP/idP.
+\end{lstlisting}
+transforms the goal
+\ssrL+~~ (b1 || b2)= b3+
+ into two subgoals, respectively
+ \ssrL+~~  (b1 || b2) -> b3+ and \\
+\ssrL+b3 -> ~~  (b1 || b2).+
+
+The same goal can be decomposed in several ways, and the user may
+choose the most convenient interpretation. For instance, the tactic:
+\begin{lstlisting}
+  apply/norP/idP.
+\end{lstlisting}
+applied on the same goal \ssrL+~~ (b1 || b2) = b3+ generates the subgoals
+\ssrL+~~  b1 /\ ~~  b2 -> b3+ and\\
+\ssrL+b3 -> ~~  b1 /\ ~~  b2+.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Declaring new \ssrC{Hint View}s}\label{ssec:vhints}
+\idxC{Hint View}
+
+The database of hints for the view mechanism is extensible via a
+dedicated vernacular command. As library {\tt ssrbool.v} already
+declares a corpus of hints, this feature is probably useful only for
+users who define their own logical connectives. Users can declare
+their own hints following the syntax used in {\tt ssrbool.v}:
+
+\begin{center}
+  \ssrC{Hint View for} {\tac} \ssrC{/} \ssrN{ident} \optional{\ssrC{|}{\naturalnumber}}
+\end{center}
+
+  where {\tac}$\in \{$\ssrC{move, apply}$\}$, \ssrN{ident} is the
+name of the lemma to be declared as a hint, and ${\naturalnumber}$ a natural
+number. If \ssrL+move+ is used as {\tac}, the hint is declared for
+assumption interpretation tactics, \ssrL+apply+ declares hints for goal
+interpretations.
+Goal interpretation view hints are declared for both simple views and
+left hand side views. The optional natural number ${\naturalnumber}$ is the
+number of implicit arguments to be considered for the declared hint
+view lemma \ssrC{name_of_the_lemma}.
+
+The command:
+
+\begin{center}
+  \ssrC{Hint View for apply//} \ssrN{ident}\optional{\ssrC{|}{\naturalnumber}}.
+\end{center}
+
+with a double slash \ssrL+//+, declares hint views for right hand sides of
+double views.
+
+
+\noindent See the files {\tt ssreflect.v} and {\tt ssrbool.v} for examples.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Multiple views}\label{ssec:multiview}
+
+The hypotheses and the goal can be interpreted applying multiple views in
+sequence. Both \ssrC{move} and \ssrC{apply} can be followed by an arbitrary number
+of \ssrC{/}$\ssrN[i]{term}$. The main difference between the following two tactics
+\begin{lstlisting}
+  apply/v1/v2/v3.
+  apply/v1; apply/v2; apply/v3.
+\end{lstlisting}
+is that the former applies all the views to the principal goal.
+Applying a view with hypotheses generates new goals, and the second line
+would apply the view \ssrC{v2} to all the goals generated by \ssrC{apply/v1}.
+Note that the NO-OP intro pattern \ssrC{-} can be used to separate two
+views, making the two following examples equivalent:
+\begin{lstlisting}
+  move=> /v1; move=> /v2.
+  move=> /v1-/v2.
+\end{lstlisting}
+
+The tactic \ssrC{move} can be used together with the \ssrC{in}
+tactical to pass a given hypothesis to a lemma. For example, if
+\ssrC{P2Q : P -> Q } and \ssrC{Q2R : Q -> R}, the following
+tactic turns the hypothesis \ssrC{p : P} into \ssrC{P : R}.
+\begin{lstlisting}
+  move/P2Q/Q2R in p.
+\end{lstlisting}
+
+If the list of views is of length two, \ssrC{Hint View}s for interpreting
+equivalences are indeed taken into account, otherwise only single
+\ssrC{Hint View}s are used.
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{\ssr{} searching tool}
+\idxC{Search \dots{}}
+
+\ssr{} proposes an extension of the \ssrC{Search} command. Its syntax is:
+
+\begin{center}
+	\ssrC{Search} \optional{\ssrN{pattern}} \optional{\optional{\ssrC{\-}} \optional{\ssrN{string}\optional{\ssrC{\%}\ssrN{key}} {\optsep} \ssrN{pattern}}}$^*$ \optional{\ssrC{in} \optional{\optional{\ssrC{\-}} \ssrN{name} }$^+$}
+\end{center}
+
+% \begin{lstlisting}
+%   Search [[\~]\ssrN{string}]$^*$ [\ssrN{pattern}] [[$\ssrN[1]{pattern} \dots $ $\ssrN[n]{pattern}$]] $[[$inside$|$outside$]$ $M_1 \dots M_n$].
+% \end{lstlisting}
+
+% This tactic returns the list of defined constants matching the
+%  given criteria:
+% \begin{itemize}
+% \item \ssrL+[[-]\ssrN{string}]$^*$+ is an open sequence of strings, which sould
+%   all appear in the name of the returned constants. The optional \ssrL+-+
+%   prefixes strings that are required  \emph{not} to appear.
+% % \item \ssrN{pattern} should be a subterm of the
+% %   \emph{conclusion} of the lemmas found by the command. If a lemma features
+% %   an occurrence
+% %   of this pattern only in one or several of its assumptions, it will not be
+% %   selected by the searching tool.
+% \item
+% \ssrL=[$\ssrN{pattern}^+$]=
+% is a list of \ssr{} terms, which may
+% include types, that are required to appear in the returned constants.
+% Terms with holes should be surrounded by parentheses.
+% \item $\ssrC{in}\ [[\ssrC{\-}]M]^+$ limits the search to the signature
+%   of open modules given in the list, but the ones preceeded by the
+%   $\ssrC{\-}$ flag. The
+%   command:
+% \begin{lstlisting}
+%   Search in M.
+% \end{lstlisting}
+% is hence a way of obtaining the complete signature of the module \ssrL{M}.
+% \end{itemize}
+where \ssrN{name} is the name of an open module.
+This command search returns the list of lemmas:
+\begin{itemize}
+\item whose \emph{conclusion} contains a subterm matching the optional
+  first \ssrN{pattern}. A $\ssrC{-}$ reverses the test, producing the list
+  of lemmas whose conclusion does not contain any subterm matching
+  the pattern;
+\item whose name contains the given string. A $\ssrC{-}$ prefix reverses
+  the test, producing the list of lemmas whose name does not contain the
+  string. A string that contains symbols or
+is followed by a scope \ssrN{key}, is interpreted as the constant whose
+notation involves that string (e.g., \ssrL=+= for \ssrL+addn+), if this is
+unambiguous; otherwise the diagnostic includes the output of the
+\ssrC{Locate} vernacular command.
+
+\item whose statement, including assumptions and types, contains a
+  subterm matching the next patterns. If a pattern is prefixed by
+  $\ssrC{-}$, the test is reversed;
+\item contained in the given list of modules, except the ones in the
+  modules prefixed by a $\ssrC{-}$.
+\end{itemize}
+
+Note that:
+\begin{itemize}
+\item As for regular terms, patterns can feature scope
+  indications. For instance, the command:
+\begin{lstlisting}
+  Search _ (_ + _)%N.
+\end{lstlisting}
+lists all the lemmas whose statement (conclusion or hypotheses)
+involve an application of the binary operation denoted by the infix
+\ssrC{+} symbol in the \ssrC{N} scope (which is \ssr{} scope for natural numbers).
+\item Patterns with holes should be surrounded by parentheses.
+\item Search always volunteers the expansion of the notation, avoiding the
+  need to execute Locate independently. Moreover, a string fragment
+  looks for any notation that contains fragment as
+  a substring. If the \ssrL+ssrbool+ library is imported, the command:
+\begin{lstlisting}
+  Search "~~".
+\end{lstlisting}
+answers :
+\begin{lstlisting}
+"~~" is part of notation (~~ _)
+In bool_scope, (~~ b) denotes negb b
+negbT  forall b : bool, b = false -> ~~ b
+contra  forall c b : bool, (c -> b) -> ~~ b -> ~~ c
+introN  forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~ b
+\end{lstlisting}
+ \item A diagnostic is issued if there are different matching notations;
+  it is an error if all matches are partial.
+\item Similarly, a diagnostic warns about multiple interpretations, and
+  signals an error if there is no default one.
+\item The command  \ssrC{Search in M.}
+is a way of obtaining the complete signature of the module \ssrL{M}.
+\item Strings and pattern indications can be interleaved, but the
+  first indication has a special status if it is a pattern, and only
+  filters the conclusion of lemmas:
+\begin{itemize}
+  \item The command :
+    \begin{lstlisting}
+      Search (_ =1 _) "bij".
+    \end{lstlisting}
+lists all the lemmas whose conclusion features a '$\ssrC{=1}$' and whose
+name contains the string \verb+bij+.
+\item The command :
+    \begin{lstlisting}
+      Search  "bij" (_ =1 _).
+    \end{lstlisting}
+lists all the lemmas whose statement, including hypotheses, features a
+'$\ssrC{=1}$' and whose name contains the string \verb+bij+.
+
+\end{itemize}
+
+\end{itemize}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Synopsis and Index}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Parameters}
+
+\begin{minipage}[c]{\textwidth}\renewcommand{\footnoterule}{}
+\begin{longtable}{lcl}
+\ssrN{d-tactic} && one of the
+  \ssrC{elim}, \ssrC{case}, \ssrC{congr}, \ssrC{apply}, \ssrC{exact}
+  and \ssrC{move} \ssr{} tactics \\
+\ssrN{fix-body} && standard \Coq{} \textit{fix\_body}\\
+\ssrN{ident} && standard \Coq{} identifier\\
+\ssrN{int} && integer literal \\
+\ssrN{key} && notation scope\\
+\ssrN{name} && module name\\
+${\naturalnumber}$ && \ssrN{int} or Ltac variable denoting a standard \Coq{} numeral\footnote{The name of this Ltac variable should not be the name of a tactic which can be followed by a bracket
+  \ssrL+[+, like  \ssrL+do+, \ssrL+ have+,\dots}\\
+\ssrN{pattern} && synonym for {\term}\\
+\ssrN{string} && standard \Coq{} string\\
+{\tac} && standard \Coq{} tactic or \ssr{} tactic\\
+{\term} & \hspace{1cm} & Gallina term, possibly containing wildcards\\
+%\ssrN{view} && global constant\\
+\end{longtable}
+\end{minipage}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Items and switches}
+
+\begin{longtable}{lclr}
+\ssrN{binder}  & {\ident} {\optsep} \ssrC{(} {\ident} \optional{\ssrC{:} {\term} } \ssrC{)} & binder& p. \pageref{ssec:pose}\\
+\\
+\ssrN{clear-switch} & \ssrC{\{} {\ident}$^+$ \ssrC{\}} & clear switch & p. \pageref{ssec:discharge}\\
+\\
+\ssrN{c-pattern} & \optional{{\term} \ssrC{in} {\optsep} {\term} \ssrC{as}} {\ident} \ssrC{in} {\term} & context pattern & p. \pageref{ssec:rewp} \\
+\\
+\ssrN{d-item} & \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{{\term} {\optsep} \ssrC{(}\ssrN{c-pattern}\ssrC{)}} & discharge item & p. \pageref{ssec:discharge}\\
+\\
+\ssrN{gen-item}  & \optional{\ssrC{@}}{\ident} {\optsep} \ssrC{(}{\ident}\ssrC{)} {\optsep} \ssrC{(}\optional{\ssrC{@}}{\ident} \ssrC{:=} \ssrN{c-pattern}\ssrC{)} & generalization item & p. \pageref{ssec:struct}\\
+\\
+\ssrN{i-pattern} & {\ident} {\optsep} \ssrC{_} {\optsep} \ssrC{?} {\optsep} \ssrC{*} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{->} {\optsep} \optional{\ssrN{occ-switch}}\ssrC{<-} {\optsep} &  intro pattern & p. \pageref{ssec:intro}\\
+& \ssrC{[} \ssrN{i-item}$^*$ \ssrC{|} $\dots$ \ssrC{|} \ssrN{i-item}$^*$ \ssrC{]} {\optsep} \ssrC{-} {\optsep} \ssrC{[:} {\ident}$^+$\ssrC{]} &\\
+\\
+\ssrN{i-item} & \ssrN{clear-switch} {\optsep} \ssrN{s-item} {\optsep} \ssrN{i-pattern} {\optsep} \ssrC{/}{\term} & intro item & p. \pageref{ssec:intro}\\
+\\
+\ssrN{int-mult} & \optional{{\naturalnumber}} \ssrN{mult-mark} & multiplier & p. \pageref{ssec:iter}\\
+\\
+\ssrN{occ-switch} & \ssrC{\{} \optional{\ssrC{+} {\optsep} \ssrC{-}} {\naturalnumber}$^*$\ssrC{\}} & occur. switch &  p. \pageref{sssec:occselect}\\
+\\
+\ssrN{mult} & \optional{{\naturalnumber}} \ssrN{mult-mark} & multiplier & p. \pageref{ssec:iter}\\
+\\
+\ssrN{mult-mark} &  \ssrC{?} {\optsep} \ssrC{!} & multiplier mark &  p. \pageref{ssec:iter}\\
+\\
+\ssrN{r-item} &  \optional{\ssrC{/}} {\term} {\optsep} \ssrN{s-item} & rewrite item & p. \pageref{ssec:extrw}\\
+\\
+\ssrN{r-prefix} & \optional{\ssrC{-}} \optional{\ssrN{int-mult}} \optional{\ssrN{occ-switch} {\optsep} \ssrN{clear-switch}} \optional{\ssrC{[}\ssrN{r-pattern}\ssrC{]}} & rewrite prefix & p. \pageref{ssec:extrw}\\
+\\
+\ssrN{r-pattern} & {\term} {\optsep} \ssrN{c-pattern} {\optsep} \ssrC{in} \optional{{\ident} \ssrC{in}} {\term} & rewrite pattern & p. \pageref{ssec:extrw}\\
+\\
+\ssrN{r-step} & \optional{\ssrN{r-prefix}}\ssrN{r-item} & rewrite step & p. \pageref{ssec:extrw}\\
+\\
+\ssrN{s-item} & \ssrC{/=} {\optsep} \ssrC{//} {\optsep} \ssrC{//=} & simplify switch & p. \pageref{ssec:intro}\\
+\\
+\end{longtable}
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Tactics}
+\emph{Note}: \ssrC{without loss} and \ssrC{suffices} are synonyms for \ssrC{wlog} and
+\ssrC{suff} respectively.
+
+\begin{longtable}{llr}
+\ssrC{move} & \textcolor{dkblue}{\texttt{idtac}} or \ssrC{hnf}& p. \pageref{ssec:profstack} \\
+\ssrC{apply} & application & p. \pageref{ssec:basictac}\\
+\ssrC{exact} &&\\
+\ssrC{abstract} && p. \pageref{ssec:abstract}, \pageref{sec:havetransparent}\\
+\\
+\ssrC{elim} & induction & p. \pageref{ssec:basictac}\\
+\ssrC{case} & case analysis  & p. \pageref{ssec:basictac}\\
+\\
+\ssrC{rewrite} \ssrN{rstep}$^+$ & rewrite& p. \pageref{ssec:extrw}\\
+\\
+\ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{s-item} {\optsep} \ssrN{binder}$^+$} \optional{\ssrC{:} {\term}} \ssrC{:=} {\term} & forward & p. \pageref{ssec:struct}\\
+\ssrC{have} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{s-item}{\optsep} \ssrN{binder}$^+$} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & chaining & \\
+\ssrC{have suff} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \optional{\ssrC{:} {\term}} \ssrC{:=} {\term} & & \\
+\ssrC{have suff} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & & \\
+\ssrC{gen have} \optional{{\ident}\ssrC{,}} \optional{\ssrN{i-pattern}} \ssrC{:} \ssrN{gen-item}$^+$ \ssrC{/} {\term} \optional{\ssrC{by} {\tac}} & & \\
+\\
+\ssrC{wlog} \optional{\ssrC{suff}} \optional{\ssrN{i-item}} \ssrC{:} \optional{\ssrN{gen-item}{\optsep} \ssrN{clear-switch}}$^*$ \ssrC{/} {\term} & specializing &  p. \pageref{ssec:struct} \\
+\\
+\ssrC{suff} \ssrN{i-item}$^*$ \optional{\ssrN{i-pattern}} \optional{\ssrN{binder}$^+$} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & backchaining & p. \pageref{ssec:struct}\\
+\ssrC{suff} \optional{\ssrC{have}} \optional{\ssrN{clear-switch}} \optional{\ssrN{i-pattern}} \ssrC{:} {\term} \optional{\ssrC{by} {\tac}} & & \\
+\\
+\ssrC{pose} {\ident} \ssrC{:=} {\term} & local definition& p. \pageref{ssec:pose}\\
+\ssrC{pose} {\ident} \ssrN{binder}$^+$ \ssrC{:=} {\term} & \rlap{local function definition}& \\
+\ssrC{pose fix} \ssrN{fix-body} & \rlap{local fix definition} & \\
+\ssrC{pose cofix} \ssrN{fix-body} & \rlap{local cofix definition} &  \\
+\\
+\ssrC{set} {\ident} \optional{\ssrC{:} {\term}} \ssrC{:=} \optional{\ssrN{occ-switch}} \optional{{\term}{\optsep} \ssrC{(}\ssrN{c-pattern}\ssrC{)}} & abbreviation&p. \pageref{ssec:set}\\
+\\
+\ssrC{unlock} \optional{\ssrN{r-prefix}]{\ident}}$^*$ & unlock & p. \pageref{ssec:lock}\\
+\\
+\ssrC{congr} \optional{\naturalnumber} {\term} & congruence& p. \pageref{ssec:congr}\\
+\end{longtable}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Tacticals}
+
+\begin{longtable}{lclr}
+\ssrN{d-tactic} \optional{\ident} \ssrC{:} \ssrN{d-item}$^{+}$ \optional{\ssrN{clear-switch}} & & discharge &  p. \pageref{ssec:discharge}\\
+\\
+{\tac} \ssrC{=>} \ssrN{i-item}$^+$ && introduction & p. \pageref{ssec:intro}\\
+\\
+{\tac} \ssrC{in} \optional{\ssrN{gen-item} {\optsep} \ssrN{clear-switch}}$^+$  \optional{\ssrC{*}} && localization & p. \pageref{ssec:gloc}\\
+\\
+\ssrC{do} \optional{\ssrN{mult}} \ssrC{[} \nelist{\tac}{|} \ssrC{]}&& iteration & p. \pageref{ssec:iter}\\
+\ssrC{do} \ssrN{mult} {\tac} &&& \\
+\\
+{\tac} \ssrC{ ; first} \optional{\naturalnumber} \ssrC{[}\nelist{\tac}{|}\ssrC{]} && selector & p. \pageref{ssec:select}\\
+{\tac} \ssrC{ ; last}  \optional{\naturalnumber} \ssrC{[}\nelist{\tac}{|}\ssrC{]} \\
+{\tac} \ssrC{ ; first} \optional{\naturalnumber} \ssrC{last} && subgoals & p. \pageref{ssec:select}\\
+{\tac} \ssrC{; last} \optional{\naturalnumber} \ssrC{first} && rotation & \\
+\\
+\ssrC{by [} \nelist{\tac}{|} \ssrC{]} && closing & p. \pageref{ssec:termin}\\
+\ssrC{by []} \\
+\ssrC{by} {\tac} \\
+\end{longtable}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection*{Commands}
+\begin{longtable}{lclr}
+\ssrL+Hint View for+ \optional{\ssrL+move+ {\it |} \ssrL+apply+} {\tt /} {\ident} \optional{{\tt|} {\naturalnumber}} && view hint
+declaration & p. \pageref{ssec:vhints}\\
+\\
+\ssrL+Hint View for apply//+ {\ident} \optional{{\tt|}{\naturalnumber}} && right hand side double
+ & p. \pageref{ssec:vhints}\\
+&&  view hint declaration &\\
+\\
+%\ssrL+Import Prenex Implicits+ && enable prenex implicits &
+%p. \pageref{ssec:parampoly}\\
+%\\
+\ssrL+Prenex Implicits+ {\ident}$^+$ & \hspace{.6cm} & prenex implicits decl.
+ & p. \pageref{ssec:parampoly}\\
+
+\end{longtable}
+
+\iffalse
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\section{Changes}
+
+\subsection{\ssr{} version 1.3}
+All changes are retrocompatible extensions but for:
+\begin{itemize}
+\item Occurrences in the type family switch now refer only to the goal, while
+      before they used to refer also to the types in the abstractions of the
+      predicate used by the eliminator. This bug used to affect lemmas like
+      \ssrC{boolP}. See the relative comments in \ssrC{ssrbool.v}.
+\item Clear switches can only mention existing hypothesis and
+      otherwise fail. This can in particular affect intro patterns
+      simultaneously applied to several goals.
+      % commit: 2686
+\item A bug in the \ssrC{rewrite} tactic allowed to
+      instantiate existential metavariables occurring in the goal.
+      This is not the case any longer (see section~\ref{ssec:rewcaveats}).
+\item The \ssrC{fold} and \ssrC{unfold} \ssrN{r-items} for \ssrC{rewrite} used to
+      fail silently when used in combination with a \ssrN{r-pattern} matching no
+      goal subterm. They now fail. The old behavior can be obtained using
+      the \ssrC{?} multiplier (see section~\ref{ssec:extrw}).
+\item \Coq{} 8.2 users with a statically linked toplevel must comment out the\\
+      \ssrC{Declare ML Module "ssreflect".}\\
+      line at the beginning of \ssrC{ssreflect.v} to compile the 1.3 library.
+\end{itemize}
+New features:
+\begin{itemize}
+\item Contextual \ssrC{rewrite} patterns.
+      The context surrounding the redex can now be used to specify which
+      redex occurrences should be rewritten (see section~\ref{ssec:rewp}).\\
+      \ssrC{rewrite [in X in _ = X]addnC.}
+      % commit: 2690, 2689, 2718, 2733
+\item Proof irrelevant interpretation of goals with existential metavariables.
+      Goals containing an existential metavariable of sort \ssrC{Prop} are
+      generalized over it, and a new goal for the missing subproof is
+      generated (see page~\pageref{sssec:apply} and
+      section~\ref{ssec:rewcaveats}).\\
+      \ssrC{apply: (ex_intro _ (@Ordinal _ y _)).}\\
+      \ssrC{rewrite insubT.}
+      % commit: 2553, 2544, 2543, 2733
+\item Views are now part of \ssrN{i-pattern} and can thus be used
+      inside intro patterns (see section~\ref{ssec:intro}).\\
+      \ssrC{move=> a b /andP [Ha Hb].}
+      % commit: 2720
+\item Multiple views for \ssrC{move}, \ssrC{move $\dots$ in} and \ssrC{apply}
+      (see section~\ref{ssec:multiview}).\\
+      \ssrC{move/v1/v2/v3.}\\
+      \ssrC{move/v1/v2/v3 in H.}\\
+      \ssrC{apply/v1/v2/v3.}
+      % commit: 2720
+\item \ssrC{have} and \ssrC{suff} idiom with view (see section~\ref{sssec:hypview}).
+\begin{lstlisting}
+  Lemma |*test*| (a b : bool) (pab : a && b) : b.
+  have {pab} /= /andP [pa ->] // : true && (a && b) := pab.
+\end{lstlisting}
+      % commit: 2726
+\item \ssrC{have suff}, \ssrC{suff have} and \ssrC{wlog suff} forward reasoning
+      tactics (see section~\ref{ssec:struct}).\\
+      \ssrC{have suff H : P.}
+      % commit: 2633
+\item Binders support in \ssrC{have} (see section~\ref{sssec:have}).\\
+      \ssrC{have H x y (r : R x y) : P x -> Q y.}
+      % commit: 2633
+\item Deferred clear switches. Clears are deferred to the end of the
+      intro pattern. In the meanwhile, cleared variables are still
+      part of the context, thus the goal can mention them, but are
+      renamed to non accessible dummy names (see section~\ref{ssec:intro}).\\
+      \ssrC{suff: G \\x H = K; first case/dprodP=> \{G H\} [[G H -> -> defK]].}
+      % commit: 2660
+\item Relaxed alternation condition in intro patterns. The
+      \ssrN{i-item} grammar rule is simplified (see section~\ref{ssec:intro}).\\
+       \ssrC{move=> a \{H\} /= \{H1\} // b c /= \{H2\}.}
+      % commit: 2713
+\item Occurrence selection for \ssrC{->} and \ssrC{<-} intro pattern
+       (see section~\ref{ssec:intro}).\\
+      \ssrC{move=> a b H \{2\}->.}
+      % commit: 2714
+\item Modifiers for the discharging '\ssrC{:}' and \ssrC{in} tactical to override
+      the default behavior when dealing with local definitions (let-in):
+      \ssrC{@f} forces the body of \ssrC{f} to be kept, \ssrC{(f)} forces the body of
+      \ssrC{f} to be dropped  (see sections~\ref{ssec:discharge}
+      and~\ref{ssec:gloc}).\\
+      \ssrC{move: x y @f z.}\\
+      \ssrC{rewrite rule in (f) $\;\;$H.}
+      %commit: 2659, 2710
+\item Type family switch in \ssrC{elim} and \ssrC{case}
+      can contain patterns with occurrence switch
+      (see section~\ref{ssec:typefam}).\\
+      \ssrC{case: \{2\}(_ == x) / eqP.}
+      % commit: 2593, 2598, 2539, 2538, 2527, 2529
+\item Generic second order predicate support for \ssrC{elim}
+      (see section~\ref{sec:views}).\\
+      \ssrC{elim/big\_prop: _}
+      % commit: 2767
+\item The \ssrC{congr} tactic now also works on products (see
+      section~\ref{ssec:congr}).
+\begin{lstlisting}
+  Lemma |*test*| x (H : P x) : P y.
+  congr (P _): H.
+\end{lstlisting}
+      % commit: 2608
+\item Selectors now support Ltac variables
+      (see section~\ref{ssec:select}).\\
+      \ssrC{let n := 3 in tac; first n last.}
+      % commit: 2725
+\item Deprecated use of \ssrC{Import Prenex Implicits} directive.
+      It must be replaced with the \Coq{} \ssrC{Unset Printing
+        Implicit Defensive} vernacular command.
+\item New synonym \ssrC{Canonical} for \ssrC{Canonical Structure}.
+\end{itemize}
+\subsection{\ssr{} version 1.4}
+New features:
+\begin{itemize}
+\item User definable recurrent contexts (see section~\ref{ssec:rewp}).\\
+      \ssrC{Notation RHS := (X in _ = X)\%pattern}
+\item Contextual patterns in
+      \ssrC{set} and `\ssrC{:}' (see section~\ref{ssec:rewp}).\\
+      \ssrC{set t := (a + _ in RHS)}
+\item NO-OP intro pattern (see section~\ref{ssec:intro}).\\
+      \ssrC{move=> /eqP-H /fooP-/barP}
+\item \ssrC{if $\ {\term}\ $ isn't $\ \ssrN{pattern}\ $ then $\ {\term}\ $
+  else $\ {\term}\ $} notation (see section~\ref{ssec:patcond}).\\
+      \ssrC{if x isn't Some y then simple else complex y}
+\end{itemize}
+\subsection{\ssr{} version 1.5}
+Incompatibilities:
+\begin{itemize}
+\item The \ssrC{have} tactic now performs type classes resolution.  The old
+	behavior can be restored with \ssrC{Set SsrHave NoTCResolution}
+\end{itemize}
+Fixes:
+\begin{itemize}
+\item The \ssrC{let foo := type of t in} syntax of standard \ssrC{Ltac} has
+	been made compatible with \ssr{} and can be freely used even if
+	the \ssr{} plugin is loaded
+\end{itemize}
+New features:
+\begin{itemize}
+\item Generalizations supported in have (see section~\ref{ssec:struct}).\\
+      \ssrC{generally have hx2px, pa : a ha / P a.}
+\item Renaming and patterns in wlog (see section~\ref{ssec:struct} and
+  page \pageref{par:advancedgen}).\\
+      \ssrC{wlog H : (n := m)$\;$ (x := m + _)$\;$ / T x}.\\
+      \ssrC{wlog H : (n := m)$\;$ (@ldef := secdef m)$\;$ / T x}.
+\item Renaming, patterns and clear switches in \ssrC{in}
+      tactical (see section~\ref{ssec:gloc}).\\
+      \ssrC{$\dots$ in H1 \{H2\} (n := m).}
+\item Handling of type classes in \ssrC{have}
+	(see page~\pageref{ssec:havetcresolution}).\\
+	\ssrC{have foo : ty. (* TC inference for ty *)}\\
+	\ssrC{have foo : ty := . (* no TC inference for ty *)}\\
+	\ssrC{have foo : ty := t. (* no TC inference for ty and t *)}\\
+	\ssrC{have foo := t. (* no TC inference for t *)}
+\item Transparent flag for \ssrC{have} to generate a \ssrC{let in} context entry
+	(see page~\pageref{sec:havetransparent}).\\
+        \ssrC{have @i : 'I\_n by apply: (Sub m); auto.}
+\item Intro pattern \ssrC{[: foo bar ]} to create abstract variables
+	(see page~\pageref{ssec:introabstract}).
+\item Tactic \ssrC{abstract:} to assign an abstract variable
+	(see page~\pageref{ssec:abstract}).\\
+  \ssrC{have [: blurb ] @i : 'I\_n by apply: (Sub m); abstract: blurb; auto.}\\
+  \ssrC{have [: blurb ] i : 'I\_n := Sub m  blurb; first by auto.}
+
+\end{itemize}
+
+\fi
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 291c07de4..fc1c01cf2 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -22,6 +22,17 @@
 \usepackage{xspace}
 \usepackage{pmboxdraw}
 \usepackage{float}
+\usepackage{color}
+  \definecolor{dkblue}{rgb}{0,0.1,0.5}
+  \definecolor{lightblue}{rgb}{0,0.5,0.5}
+  \definecolor{dkgreen}{rgb}{0,0.4,0}
+  \definecolor{dk2green}{rgb}{0.4,0,0}
+  \definecolor{dkviolet}{rgb}{0.6,0,0.8}
+  \definecolor{dkpink}{rgb}{0.2,0,0.6}
+\usepackage{listings}
+  \def\lstlanguagefiles{coq-listing.tex}
+\usepackage{tabularx}
+\usepackage{array,longtable}
 
 \floatstyle{boxed} 
 \restylefloat{figure}
@@ -99,6 +110,11 @@ Options A and B of the licence are {\em not} elected.}
 \include{RefMan-ltac.v}% Writing tactics
 \include{RefMan-tacex.v}% Detailed Examples of tactics
 
+\lstset{language=SSR}
+\lstset{moredelim=[is][]{|*}{*|}}
+\lstset{moredelim=*[is][\itshape\rmfamily]{/*}{*/}}
+\include{RefMan-ssr}
+
 \part{User extensions}
 \include{RefMan-syn.v}% The Syntax and the Grammar commands
 %%SUPPRIME \include{RefMan-tus.v}% Writing tactics
diff --git a/doc/refman/coq-listing.tex b/doc/refman/coq-listing.tex
new file mode 100644
index 000000000..c69c3b1b8
--- /dev/null
+++ b/doc/refman/coq-listing.tex
@@ -0,0 +1,152 @@
+%=======================================================================
+% Listings LaTeX package style for Gallina + SSReflect (Assia Mahboubi 2007)
+
+\lstdefinelanguage{SSR} {
+
+% Anything betweeen $ becomes LaTeX math mode
+mathescape=true,
+% Comments may or not include Latex commands
+texcl=false,
+
+
+% Vernacular commands
+morekeywords=[1]{
+From, Section, Module, End, Require, Import, Export, Defensive, Function,
+Variable, Variables, Parameter, Parameters, Axiom, Hypothesis, Hypotheses,
+Notation, Local, Tactic, Reserved, Scope, Open, Close, Bind, Delimit,
+Definition, Let, Ltac, Fixpoint, CoFixpoint, Add, Morphism, Relation,
+Implicit, Arguments, Set, Unset, Contextual, Strict, Prenex, Implicits,
+Inductive, CoInductive, Record, Structure, Canonical, Coercion,
+Theorem, Lemma, Corollary, Proposition, Fact, Remark, Example,
+Proof, Goal, Save, Qed, Defined, Hint, Resolve, Rewrite, View,
+Search, Show, Print, Printing, All, Graph, Projections, inside,
+outside, Locate, Maximal},
+
+% Gallina
+morekeywords=[2]{forall, exists, exists2, fun, fix, cofix, struct,
+      match, with, end, as, in, return, let, if, is, then, else,
+      for, of, nosimpl},
+
+% Sorts
+morekeywords=[3]{Type, Prop},
+
+% Various tactics, some are std Coq subsumed by ssr, for the manual purpose
+morekeywords=[4]{
+         pose, set, move, case, elim, apply, clear,
+            hnf, intro, intros, generalize, rename, pattern, after,
+	    destruct, induction, using, refine, inversion, injection,
+         rewrite, congr, unlock, compute, ring, field,
+            replace, fold, unfold, change, cutrewrite, simpl,
+         have, gen, generally, suff, wlog, suffices, without, loss, nat_norm,
+            assert, cut, trivial, revert, bool_congr, nat_congr, abstract,
+	 symmetry, transitivity, auto, split, left, right, autorewrite},
+
+% Terminators
+morekeywords=[5]{
+         by, done, exact, reflexivity, tauto, romega, omega,
+         assumption, solve, contradiction, discriminate},
+
+
+% Control
+morekeywords=[6]{do, last, first, try, idtac, repeat},
+
+% Various symbols
+% For the ssr manual we turn off the prettyprint of formulas
+% literate=
+%	{->}{{$\rightarrow\,$}}2
+% 	{->}{{\tt ->}}3
+%	{<-}{{$\leftarrow\,$}}2
+% 	{<-}{{\tt <-}}2
+% 	{>->}{{$\mapsto$}}3
+% 	{<=}{{$\leq$}}1
+% 	{>=}{{$\geq$}}1
+% 	{<>}{{$\neq$}}1
+% 	{/\\}{{$\wedge$}}2
+% 	{\\/}{{$\vee$}}2
+% 	{<->}{{$\leftrightarrow\;$}}3
+% 	{<=>}{{$\Leftrightarrow\;$}}3
+% 	{:nat}{{$~\in\mathbb{N}$}}3
+%	{fforall\ }{{$\forall_f\,$}}1
+%	{forall\ }{{$\forall\,$}}1
+%	{exists\ }{{$\exists\,$}}1
+% 	{negb}{{$\neg$}}1
+% 	{spp}{{:*:\,}}1
+% 	{~}{{$\sim$}}1
+% 	{\\in}{{$\in\;$}}1
+% 	{/\\}{$\land\,$}1
+% 	{:*:}{{$*$}}2
+%	{=>}{{$\,\Rightarrow\ $}}1
+% 	{=>}{{\tt =>}}2
+% 	{:=}{{{\tt:=}\,\,}}2
+% 	{==}{{$\equiv$}\,}2
+% 	{!=}{{$\neq$}\,}2
+% 	{^-1}{{$^{-1}$}}1
+% 	{elt'}{elt'}1
+%       {=}{{\tt=}\,\,}2
+%       {+}{{\tt+}\,\,}2,
+literate=
+	{isn't }{{{\ttfamily\color{dkgreen} isn't }}}1,
+
+% Comments delimiters, we do turn this off for the manual
+%comment=[s]{(*}{*)},
+
+% Spaces are not displayed as a special character
+showstringspaces=false,
+
+% String delimiters
+morestring=[b]",
+morestring=[d]",
+
+% Size of tabulations
+tabsize=3,
+
+% Enables ASCII chars 128 to 255
+extendedchars=true,
+
+% Case sensitivity
+sensitive=true,
+
+% Automatic breaking of long lines
+breaklines=true,
+
+% Default style fors listings
+basicstyle=\ttfamily,
+
+% Position of captions is bottom
+captionpos=b,
+
+% Full flexible columns
+columns=[l]fullflexible,
+
+% Style for (listings') identifiers
+identifierstyle={\ttfamily\color{black}},
+% Note : highlighting of Coq identifiers is done through a new
+% delimiter definition through an lstset at the begining of the
+% document. Don't know how to do better.
+
+% Style for declaration keywords
+keywordstyle=[1]{\ttfamily\color{dkviolet}},
+
+% Style for gallina keywords
+keywordstyle=[2]{\ttfamily\color{dkgreen}},
+
+% Style for sorts keywords
+keywordstyle=[3]{\ttfamily\color{lightblue}},
+
+% Style for tactics keywords
+keywordstyle=[4]{\ttfamily\color{dkblue}},
+
+% Style for terminators keywords
+keywordstyle=[5]{\ttfamily\color{red}},
+
+
+%Style for iterators
+keywordstyle=[6]{\ttfamily\color{dkpink}},
+
+% Style for strings
+stringstyle=\ttfamily,
+
+% Style for comments
+commentstyle=\rmfamily,
+
+}