diff options
author | 2017-09-08 19:12:37 +0200 | |
---|---|---|
committer | 2017-09-08 19:12:37 +0200 | |
commit | d4f081ffa94b1e9719f8ee6a9ca8da2c73e8a39a (patch) | |
tree | ee1f39bdaeaf79c380a839992040bfaaa290169e /doc | |
parent | b1fbec7e3945fe2965f4ba9f80c8c31b821dbce1 (diff) |
Fix the introduction of SSR refman chapter.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-ssr.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index 61f7421c4..db794e5a6 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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |