diff options
| author | Pierre Letouzey | 2014-12-09 12:00:10 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 12:14:41 +0100 |
| commit | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (patch) | |
| tree | 52eee33926e6791b4d2ac23c04f48404057899b4 /doc/refman/AddRefMan-pre.tex | |
| parent | 56302f63809494946adf4e805bc61d55ed9d6f14 (diff) | |
refman: switch all source files to utf8
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
Diffstat (limited to 'doc/refman/AddRefMan-pre.tex')
| -rw-r--r-- | doc/refman/AddRefMan-pre.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/refman/AddRefMan-pre.tex b/doc/refman/AddRefMan-pre.tex index 461e8e6d0c..eee41a6798 100644 --- a/doc/refman/AddRefMan-pre.tex +++ b/doc/refman/AddRefMan-pre.tex @@ -18,15 +18,15 @@ Manual. and Hugo Herbelin. \item[Implicit coercions] This chapter details the use of the coercion - mechanism. It is contributed by Amokrane Saïbi. + mechanism. It is contributed by Amokrane Saïbi. %\item[Proof of imperative programs] This chapter explains how to % prove properties of annotated programs with imperative features. -% It is contributed by Jean-Christophe Filliâtre +% It is contributed by Jean-Christophe Filliâtre \item[Program extraction] This chapter explains how to extract in practice ML files from $\FW$ terms. It is contributed by Jean-Christophe - Filliâtre and Pierre Letouzey. + Filliâtre and Pierre Letouzey. \item[Program] This chapter explains the use of the \texttt{Program} vernacular which allows the development of certified @@ -37,7 +37,7 @@ Manual. % manual of the tools he wrote for printing proofs in natural % language. At this time, French and English languages are supported. -\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole +\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole class of arithmetic problems. \item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This @@ -46,7 +46,7 @@ Manual. \item[The {\tt Setoid\_replace} tactic] This is a tactic to do rewriting on types equipped with specific (only partially - substitutive) equality. The chapter is contributed by Clément Renard. + substitutive) equality. The chapter is contributed by Clément Renard. \item[Calling external provers] This chapter describes several tactics which call external provers. |