Rewording the introduction

The contents should be exactly the same.

I removed the distinction between tactical and pseudo-tactical because
I think that it is too much technical for the introduction. I used
"syntactic construction" and made appeal to the reader intuition
by saying that such construction behaves similarly to a tactical.

I think the text would be much more readable if "the tactics described in
Chapter..." could be replaced by a *name*, but I'm afraid the only
one I could use (Ltac) is a bit too ambiguous.  So I'm open to suggestions.

1 files changed, 50 insertions, 37 deletions

diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index 08b6834896..61f7421c44 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -28,57 +28,70 @@
   {\end{minipage}\end{Sbox}\noindent\doublebox{\TheSbox}}
 \section{Introduction}\label{sec:intro}
 
-This chapter describes a set of tactics orginally designed to provide
-support at the tactic level for the so-called \emph{small scale
-reflection} proof methodology but which at the end provides with a
-couple of tactics and tacticals of no less general interest than other
-Coq tactics, even, if due to a development of these tactics in
-parallel from the development of the Coq tactics, there are
-redundancies. Eventually, it is the hope of the Coq development team
-that the specific features of these tactics will be united into a
-consistent set of tactics, and the superficial syntactic differences
-be cleaned.
-
-The main conceptual difference between the tactics described in this
+This chapter describes a set of tactics known as \ssr{}
+originally designed to provide support for the so-called \emph{small scale
+reflection} proof methodology.  Despite the original purpose this set of tactic
+is of general interest and is available in Coq starting from version 8.7.
+
+\ssr{} was developed independently of the tactics described in
+Chapter~\ref{Tactics}.  Indeed the scope of the tactics part of
+\ssr{} largely overlaps with the standard set of tactics.  Eventually
+the overlap will be reduced in future releases of Coq.
+
+Proofs written in \ssr{} typically look quite different from the
+ones written using only tactics as per Chapter~\ref{Tactics}.
+We try to summarise here the most ``visible'' ones in order to
+help the reader already accustomed to the tactics described in
+Chapter~\ref{Tactics}to read this chapter.
+
+The first difference between the tactics described in this
 chapter and the tactics described in Chapter~\ref{Tactics} is the way
-hypotheses are managed. In Chapter~\ref{Tactics} the most common
+hypotheses are managed (we call this \emph{bookkeeping}).
+In Chapter~\ref{Tactics} the most common
 approach is to avoid moving explicitly hypotheses back and forth
-between the context and the conclusion of the goal. On the contrary,
-for the tactics described in this Chapter, the default model is that
+between the context and the conclusion of the goal. On the contrary
+in \ssr{}
 all bookkeeping is performed on the conclusion of the goal, using for
-that purpose a couple of pseudo-tacticals or tacticals: a
-pseudo-tactical {\tt :} to move hypotheses from the context to the
-conclusion, an (almost) tactical {\tt =>} to move hypotheses from the
-conclusion to the context, and a pseudo-tactical {\tt in} to move back
+that purpose a couple of syntactic constructions behaving similar to
+tacticals (and often named as such in this chapter).
+The \ssrC{:} tactical  moves hypotheses from the context to the
+conclusion, while \ssrC{=>} moves hypotheses from the
+conclusion to the context, and \ssrC{in} moves back
 and forth an hypothesis from the context to the conclusion for the
 time of applying an action to it.
 
-While naming hypotheses is commonly done by means of an {\tt as}
-clause in the basic model of Chapter~\ref{Tactics}, it is here to {\tt
-=>} that this task is devoted. While generalizing the goal is normally
+While naming hypotheses is commonly done by means of an \ssrC{as}
+clause in the basic model of Chapter~\ref{Tactics}, it is here to
+\ssrC{=>} that this task is devoted. As tactics leave
+new assumptions in the conclusion, and are often followed by
+\ssrC{=>} to explicitly name them.
+While generalizing the goal is normally
 not explicitly needed in Chapter~\ref{Tactics}, it is an explicit
-operation performed by {\tt :}.
+operation performed by \ssrC{:}.
 
 Beside the difference of bookkeeping model, this chapter includes
 specific tactics which have no explicit counterpart in
-Chapter~\ref{Tactics} such as tactics for sharing subproofs using the
-{\tt general have} where ({\tt have} is the name given in this Chapter
-to the concept carried by the {\tt assert} tactic) and {\tt wlog}
-(shortening for {\em without loss of generality}).
+Chapter~\ref{Tactics} such as tactics to mix forward steps and
+generalizations as \ssrC{generally have} or \ssrC{without loss}.
 
-It also includes a mini-language for selection of subterms in tactics
-or pseudo-tacticals where it matters.
-
-It also adopts the point of view that rewriting, definition
+\ssr{} adopts the point of view that rewriting, definition
 expansion and partial evaluation participate all to a same concept of
-rewriting a goal in a larse sense. As such, they are all laid on the
-same keyword {\tt rewrite} using instead a symbolic syntax to
-distinguish between the different option, leading at the end to a
-compact syntax for combinations of such steps.
+rewriting a goal in a larger sense. As such, all these functionalities are
+provided by the \ssrC{rewrite} tactic.
+
+\ssrC{} includes a little language of patterns to select subterms in tactics
+or tacticals where it matters.  Its most notable application
+is in the \ssrC{rewrite} tactic, where patterns are used to specify
+where the rewriting step has to take place.
 
-Finally, it supports the so-called reflection steps, typically
+Finally, \ssr{} supports the so-called reflection steps, typically
 allowing to switch back and forth between the computational view and
-logical view at decicable connectives. % Too restrictive ?
+logical view of a concept.
+
+To conclude it is worth mentioning that \ssr{} tactics
+can be mixed with non \ssr{} tactics in the same proof,
+or in the same LTac expression.  The few exceptions
+to this statement are described in section~\label{sec:compat}.
 
 \iffalse
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%