diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 10:53:37 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-11 10:53:37 +0200 |
| commit | 75a6ad95bba622975f1978e2d72d60be2eb813d9 (patch) | |
| tree | 5cff85ab5272f94a0ecd7e516da1ee8898c6dce6 /doc | |
| parent | e22809bbe533f9dc0c36146b44ae3e6f9513cd32 (diff) | |
| parent | d4f081ffa94b1e9719f8ee6a9ca8da2c73e8a39a (diff) | |
Merge PR #1035: Fix the introduction of SSR refman chapter.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ssr.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ssr.tex b/doc/refman/RefMan-ssr.tex index 0e4d44f21..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,18 +79,18 @@ 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 +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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |