From d4f081ffa94b1e9719f8ee6a9ca8da2c73e8a39a Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 8 Sep 2017 19:12:37 +0200
Subject: Fix the introduction of SSR refman chapter.

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

(limited to 'doc/refman/RefMan-ssr.tex')

diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex
index 61f7421c44..db794e5a63 100644
--- a/doc/refman/RefMan-ssr.tex
+++ b/doc/refman/RefMan-ssr.tex
@@ -42,7 +42,7 @@ 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.
+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
@@ -79,19 +79,19 @@ expansion and partial evaluation participate all to a same concept of
 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
+\ssr{} 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, \ssr{} supports the so-called reflection steps, typically
+Finally, \ssr{} supports so-called reflection steps, typically
 allowing to switch back and forth between the computational view and
 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}.
+or in the same Ltac expression.  The few exceptions
+to this statement are described in section~\ref{sec:compat}.
 
 \iffalse
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -130,7 +130,7 @@ ProofGeneral provided in the distribution:
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection*{Acknowledgments}
-The authors would like to thank Fr\'ed\'eric Blanqui, Fran\,cois Pottier
+The authors would like to thank Frédéric Blanqui, François Pottier
 and Laurence Rideau for their comments and suggestions.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-- 
cgit v1.2.3

