diff --git a/DiaposSoutenance.tex b/DiaposSoutenance.tex
index d286fe2..c694aec 100644
--- a/DiaposSoutenance.tex
+++ b/DiaposSoutenance.tex
@@ -221,8 +221,6 @@
 			\tableofcontents[pausesections,hideallsubsections]
 		\end{multicols}
 	\end{frame}
-
-	\section{Introduction}
 	
 	\section{Featherweight Java}
 		
@@ -253,8 +251,15 @@
 				\textbf{Class table} \only<3>{$+$ \textbf{Expression} = \textbf{Programme}}
 				\begin{fjlisting}
 					\textbf{class} A \textbf{extends} Object \{...\}\\
-					\textbf{class} B \textbf{extends} Object \{...\}\\
-					\fjclass{Paire}{\fjattr{fst} \fjattr{snd}}{}\\
+					\textbf{class} B \textbf{extends} A \{...\}\\
+					\textbf{class} Paire \textbf{extends} Object \{\\
+					\null\qquad A fst;\\
+					\null\qquad B snd;\\
+					\null\qquad Paire(A fst, B snd)\{...\}\\
+					\null\qquad B getBFst()\{\\
+					\null\qquad\qquad \textbf{return} (B)this.fst;\\
+					\null\qquad\}\\
+					\}\\
 					\pause
 					\fjmain{new Paire(new A(), new B())}
 				\end{fjlisting}
@@ -279,35 +284,35 @@
 			\begin{frame}
 				\pause
 				\[\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
+				{\mathcal{A},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
 				{\fj{x} \in \Gamma}
 				\qquad
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
+				{\mathcal{A},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
+				{\mathcal{A},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
 				\]
 				\pause
 				\vspace{.2ex}
 				\[
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
-				{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
+				{\mathcal{A},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
+				{\begin{array}{c}\mathcal{A},\Gamma \Vdash e : \fj{Cc} \quad \mathcal{A},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
 				\]
 				\vspace{.2ex}
 				\[
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
+				{\mathcal{A},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
+				{\mathcal{A},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{constructor}(\fj{C}) = \overline{\fj{D}}}
 				\]
 				\vspace{.2ex}
 				\[
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
+				{\mathcal{A},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
+				{\mathcal{A},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
 				\qquad
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
+				{\mathcal{A},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
+				{\mathcal{A},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}}
 				\]
 			\end{frame}
 		
@@ -381,7 +386,7 @@
 		\subsection{Idée d'une structure}
 		\begin{frame}
 			\begin{itemize}[<+->]
-				\item Besoin de restreindre les contextes
+				\item Spécifier ce que l'on veut tester
 				\item Empêcher au test d'accéder à tout
 				\item Utiliser un mécanisme déjà là
 				\item Inspiration: \eng{header file} en C
@@ -395,22 +400,12 @@
 					\pause
 					
 					Int \{\}\\
-					Int : Int suivant(Int)\\
-					Int : Int add(Int,Int)\\
-					Int <: Number
-				\end{fjlisting}
-			\end{frame}
-			\begin{frame}
-				\begin{fjlisting}
-					Frac(Int numerateur, Int denominateur)\\
-					Frac : Frac inverted()\\
-					Frac : Int floor()\\
-					Frac <: Number\\\null
+					Int : Int add(Int)\\
+					Int <: Number\\
 					\pause
 					
-					RichInt \{Int value\}\\
-					RichInt : Int getInt()\\
-					RichInt <: Int
+					Frac (Int numerateur, Int)\\
+					RichInt \{Int value\}
 				\end{fjlisting}
 			\end{frame}
 			\begin{frame}
@@ -458,6 +453,25 @@
 		\subsection{L'opérateur d'implémentation}
 		
 			\begin{frame}
+				\[
+				\infer
+				{\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}
+				{
+					\overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)
+					\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
+				}\qquad
+				\pause
+				\infer
+				{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
+				{\begin{array}{l}
+						\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\
+						\overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\
+						\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad 
+						\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
+					\end{array}
+				}
+				\]
+				\vspace{2ex}
 				\[
 					\infer
 					{\mathcal{A} \triangleright \left[\fj{C : G m($\overline{\texttt{F}}$)}\right]}
@@ -471,25 +485,7 @@
 					{\mathcal{A} \triangleright \left[\fj{C} \subclass \fj{D}\right]}
 					{\fj{C} \subclass_\mathcal{A} \fj{D}}
 				\]
-				\pause
-				\vspace{2ex}
-				\[
-					\infer
-					{\mathcal{A} \triangleright \left[\fj{ C \{ $\overline{\texttt{E}}\;\overline{\texttt{f}}$\}}\right]}
-					{
-						\overline{\fj{F}}\;\overline{\fj{f}} \subset \operatorname{fields}_\mathcal{A}(C)
-						\quad \overline{\fj{F}}\subclass_\mathcal{A}\overline{\fj{E}}
-					}\qquad
-					\infer
-					{\mathcal{A} \triangleright \left[\fj{ C ( $\overline{\texttt{E}}\;\overline{\texttt{f}}$)}\right]}
-					{\begin{array}{l}
-							\exists \overline{\fj{f'}}\quad \overline{\fj{f0}} = \overline{\fj{f}}\boxplus\overline{\fj{f'}} \\
-							\overline{\fj{F}} = \overline{\fj{E}} \quad\text{où \fj{f} est défini} \\
-							\overline{\fj{E}} \subclass \overline{\fj{F}} \quad \land \quad 
-							\overline{\fj{F}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)
-						\end{array}
-					}
-				\]
+				
 				
 			\end{frame}
 		
@@ -555,6 +551,13 @@
 				\pause
 				\[
 				\infer
+				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
+				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
+				\]
+				\vspace{.3ex}
+				\pause
+				\[
+				\infer
 				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{x} : \Gamma(\fj{x})}
 				{\fj{x} \in \Gamma}
 				\qquad
@@ -562,7 +565,7 @@
 				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
 				{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\ \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
 				\]
-				\pause
+				\vspace{.3ex}
 				\[
 				\infer
 				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{new C(}\overline{e_x}\fj{)} : \fj{C}}
@@ -571,12 +574,6 @@
 				\vspace{.3ex}
 				\[
 				\infer
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
-				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
-				\]
-				\vspace{.3ex}
-				\[
-				\infer
 				{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}}
 				{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}}
 				\qquad