diff --git a/doc/slicing/.gitignore b/doc/slicing/.gitignore
index ed79c64d8ff52e771af67d7d1de8186cc5956922..1c8ae1c9863bb996bff694ae937acf6f9330ef2c 100644
--- a/doc/slicing/.gitignore
+++ b/doc/slicing/.gitignore
@@ -2,13 +2,12 @@ anr-logo.png
 biblio.bib
 eu-flag.jpg
 frama-c-book.cls
-frama-c-cover.pdf
-frama-c-left.pdf
-frama-c-right.pdf
-frama-c-affiliation.tex
 main.pdf
 call.pdf
 choose_call.pdf
 exple2.pdf
 propagation.pdf
 propagation.pdf
+fc-macros.tex
+logos
+frama-c-guy.png
diff --git a/doc/slicing/algo.ml b/doc/slicing/algo.ml
index a5efc17891dd2b494ea7e10f54da1ac0d2599d2e..604aff6e71df9cd0c80f37e20bd4ad4de37895c9 100644
--- a/doc/slicing/algo.ml
+++ b/doc/slicing/algo.ml
@@ -18,5 +18,6 @@ and
   let new_ff = H.replace_stmt_mark ff stmt new_m in
   let elems = H.get_elems stmt stmt_elems in
   let (_, other_elems) = List.partition (fun elem -> elem = e) elems in
-  let mark_spare_elem e ff = mark_rec_pdg_elem pdg stmt_elems H.spare_mark e ff in
+  let mark_spare_elem e ff =
+    mark_rec_pdg_elem pdg stmt_elems H.spare_mark e ff in
   List.fold_right mark_spare_elem other_elems new_ff
diff --git a/doc/slicing/interexples.tex b/doc/slicing/interexples.tex
index 20c59843be629e2d487c84fdfb95b6f1bfbc875d..9b6549d1f9f256c43c0ed48a207e78f2b9aba451 100644
--- a/doc/slicing/interexples.tex
+++ b/doc/slicing/interexples.tex
@@ -3,7 +3,7 @@
 
 Cette partie présente comment les actions élémentaires précédemment présentées
 peuvent être utilisées pour répondre à des requêtes utilisateur de plus haut
-niveau. 
+niveau.
 
 
 \section{Présentation de l'exemple}
@@ -19,10 +19,10 @@ comme on ne s'intéresse ici qu'à la propagation interprocédurale,
 on n'utilise qu'une marque élémentaire $m$ quelconque qui rend un élément
 visible et la marque \spare{} déjà mentionnée.
 
-\noindent\begin{tabular}{p{4cm}p{4.5cm}p{5cm}}
+\noindent\begin{tabular}{p{4.4cm}p{4.5cm}p{5.3cm}}
 \begin{verbatim}
 int X, Y;
-int g (int u, int v, 
+int g (int u, int v,
        int w) {
   lg1: X = u;
   lg2: Y = u + v;
@@ -32,23 +32,23 @@ int g (int u, int v,
 &
 \begin{verbatim}
 int Z;
-int f (int a, int b, 
-       int c, int d, 
+int f (int a, int b,
+       int c, int d,
        int e) {
   int r;
-  lf1: r = g (a, b, c);
-  lf2: Z = g (r, d, e);
+  lf1: r = g (a,b,c);
+  lf2: Z = g (r,d,e);
   return X;
-  }
+}
 \end{verbatim}
 &
 \begin{verbatim}
 int I, J, K, L, M, N;
 int main () {
   lm1: /* ... */
-  lm2: N = f (I, J, K, L, M);
+  lm2: N = f (I,J,K,L,M);
   lm3: /* ... */
-  }
+}
 \end{verbatim}
 \end{tabular}
 
@@ -79,7 +79,7 @@ Puis, la seconde action
 génère $\actChooseCall(c_1, f_1)$ et $\actChooseCall(c_2, f_1)$.
 
 A l'application de la première de ces nouvelles actions,
-comme il n'y a pas encore de spécialisation pour $g$, 
+comme il n'y a pas encore de spécialisation pour $g$,
 on génère~:
 
 \begin{itemize}
@@ -102,9 +102,9 @@ L'application de $\actChooseCall(c_2, f_1)$ produit~:
   \item et $\actChangeCall(c_2, f_1, g_1)$.
 \end{itemize}
 
-Comme $g_1$ est appelée en $c_1$, 
+Comme $g_1$ est appelée en $c_1$,
 la modification de son marquage conduit à générer $\actMissingInputs(c_1, f_1)$,
-qui, vues les options, est directement traduit par 
+qui, vues les options, est directement traduit par
 $\actModifCallInputs(c_1, f_1)$.
 
 Puis, le $\actChangeCall{}$ va déclencher $\actModifCallInputs(c_2, f_1)$
@@ -201,6 +201,3 @@ $m_1$ aux entrées $b$ et $d$ de $f_1$, puis aux entrées $J$ et $L$ de ${\mathi
 main}_1$.
 
 \bb{\centerline{\uneimage{exple2v4-2}}}\bb
-
-
-
diff --git a/doc/slicing/macros_slicing.tex b/doc/slicing/macros_slicing.tex
index 8e6b866c7cb643d377418cad661758f791675109..b42c920c7818d601e4e88a7eb9733261786015bd 100644
--- a/doc/slicing/macros_slicing.tex
+++ b/doc/slicing/macros_slicing.tex
@@ -7,6 +7,7 @@
 \usepackage{wasysym}
 \usepackage{stmaryrd}
 \usepackage{listings}
+\usepackage{makeidx}
 
 \usepackage[french]{varioref}
 
@@ -40,8 +41,8 @@
 
 \newcommand{\camlListingInput}[1]{
   \begin{footnotesize}
-  \lstinputlisting[language=caml,
-                  style=clststyle,
+  \lstinputlisting[language=Ocaml,
+                  style=ocaml-basic,
                   inputencoding=utf8,
                   extendedchars=true,
                   literate={ç}{{\c{c}}}1
@@ -96,9 +97,6 @@
 \newcommand{\verbtt}[1]{{\small{\tt{#1}}}}
 %------------------------------------------------------------------------------
 % Légende des figures :
-\usepackage[hang,small]{caption}
-\renewcommand{\captionfont}{\it}
-\renewcommand{\captionlabelfont}{\it \bf \small}
 %\renewcommand{\captionlabeldelim}{ : }
 %-----------------------------------------------
 % prend le nom du fichier
diff --git a/doc/slicing/main.tex b/doc/slicing/main.tex
index c7f140780c77afb2915ef487e4c36bd2e561c239..627367531a95253341797871ad4ebe2d751f228d 100644
--- a/doc/slicing/main.tex
+++ b/doc/slicing/main.tex
@@ -1,32 +1,24 @@
-\documentclass[a4paper,11pt,twoside,openright,web,lang=french]{frama-c-book}
+\documentclass[lang=french]{frama-c-book}
 
 %\usepackage[french]{babel}
 
 \input{macros_slicing.tex}
-\input{./frama-c-affiliation.tex}
 %==============================================================================
-\begin{document}
-
-\coverpage{Slicing --- Documentation technique}
 
-\begin{titlepage}
-\begin{flushleft}
-\includegraphics[height=14mm]{../images/cealistlogo.jpg}
-\end{flushleft}
-\vfill
-\title{Documentation du greffon Slicing}{Conception d'un outil de Slicing}
+\title{Greffon Slicing}
+\subtitle{Conception d'un outil de Slicing}
 \author{Anne Pacalet et Patrick Baudin}
-\begin{tabular}{l}
-  \fcaffiliationfr
-\end{tabular}
-\vfill
-\begin{flushleft}
-  \textcopyright 2006-2022 CEA LIST
 
-\end{flushleft}
-\end{titlepage}
 
-\begin{sloppypar}
+\cclicence{by-sa}
+\copyrightstarts{2006}
+
+\begin{document}
+\sloppy
+\emergencystretch 3em
+
+\maketitle
+
 \input{slicing.tex}
-\end{sloppypar}
+
 \end{document}
diff --git a/doc/slicing/projets.tex b/doc/slicing/projets.tex
index dabfdf57a982b47e52d8855a9dca8b8647246019..d136715b2b18e8e52c227a0dc31a363efc2719c8 100644
--- a/doc/slicing/projets.tex
+++ b/doc/slicing/projets.tex
@@ -202,10 +202,11 @@ dans le nouveau~:
 En effet, lors du calcul de la fonction spécialisée, on ne savait
 pas supprimer l'argument correspondant,
 mais on propageait tout de même la valeur pour supprimer les éventuelles
-branchesmortes. 
+branchesmortes.
 \begin{exemple}
 Dans l'exemple précédent,
 on peut spécialiser \verbtt{f} en \verbtt{f\_1} car on sait que $x=-1$.
+
 \begin{tabular}{ccl}
 Mais on aimerait aussi transformer &:& \verb! void f_1 (int x) { ... }!\\
 en &:& \verb! void f_1 (void) { int x = -1; ... }!
@@ -226,8 +227,8 @@ il n'y avait pas de point de programme correspondant à la branche
 Comme on l'a vu, la propagation de constante peut permettre de
 spécialiser les fonctions et de couper des branches de programme.
 
-Ce type calcul s'effectue a priori par propagation avant. 
-Pour faire de la propagation arrière, 
+Ce type calcul s'effectue a priori par propagation avant.
+Pour faire de la propagation arrière,
 nous aimerions utiliser un calcul de WP.
 
 Le principe d'utilisation serait le suivant~: