CLEANUP: putting examples inside "figure" environment

2 files changed, 262 insertions, 249 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 4066a108cd..ad711549b2 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -532,221 +532,221 @@ These inductive definitions, together with global assumptions and global definit
 Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$
 such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
 $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}.
+Figures~\ref{fig:bool}--\ref{fig:even:odd} show formal representation of several inductive definitions.
 
 \begin{latexonly}%
-\subsection*{Examples}
-
-If we take the following inductive definition (denoted in concrete syntax):
-\begin{coq_example*}
+  \newpage
+  \def\captionstrut{\vbox to 1.5em{}}
+  \newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
+    \begin{array}{r @{\mathrm{~:=~}} l}
+      #2 & #3 \\
+    \end{array}
+    \hskip-.4em
+    \right)$}
+
+  \def\colon{@{\hskip.5em:\hskip.5em}}
+
+  \begin{figure}[H]
+    \strut If we take the following inductive definition (denoted in concrete syntax):
+\begin{verbatim}
 Inductive bool : Set :=
   | true : bool
   | false : bool.
-\end{coq_example*}
-then:
-\def\colon{@{\hskip.5em:\hskip.5em}}
-\newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
-                                           \begin{array}{r @{\mathrm{~:=~}} l}
-                                              #2 & #3 \\
-                                           \end{array}
-                                           \hskip-.4em
-                                     \right)$}
-  \def\GammaI{\left[\begin{array}{r \colon l}
-                      \bool & \Set
-                    \end{array}
-              \right]}
-  \def\GammaC{\left[\begin{array}{r \colon l}
-                      \true & \bool\\
-                      \false & \bool
-                    \end{array}
-              \right]}
-  \begin{itemize}
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \bool & \Set
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r \colon l}
+                        \true & \bool\\
+                        \false & \bool
+                      \end{array}
+                \right]}
+    \begin{itemize}
     \item $p = 0$
     \item $\Gamma_I = \GammaI$
     \item $\Gamma_C = \GammaC$
-  \end{itemize}
-  and thus it enriches the global environment with the following entry:
-  \vskip.5em
-  \ind{p}{\Gamma_I}{\Gamma_C}
-  \vskip.5em
-  \noindent that is:
-  \vskip.5em
-  \ind{0}{\GammaI}{\GammaC}
-  \vskip.5em
-  \noindent In this case, $\Gamma_P=[\,]$.
-
-\vskip1em\hrule\vskip1em
-
-\noindent If we take the followig inductive definition:
-\begin{coq_example*}
+    \item $\Gamma_P=[\,]$.
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{p}{\Gamma_I}{\Gamma_C}
+    \vskip.5em
+    \noindent that is:
+    \vskip.5em
+    \ind{0}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\bool} inductive type.}
+    \label{fig:bool}
+  \end{figure}
+
+  \begin{figure}[H]
+    \strut If we take the followig inductive definition:
+\begin{verbatim}
 Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.
-\end{coq_example*}
-then:
-\def\GammaI{\left[\begin{array}{r \colon l}
-                    \nat & \Set
-                  \end{array}
-            \right]}
-\def\GammaC{\left[\begin{array}{r \colon l}
-                    \nO & \nat\\
-                    \nS & \nat\ra\nat
-                  \end{array}
-            \right]}
-\begin{itemize}
-  \item $p = 0$
-  \item $\Gamma_I = \GammaI$
-  \item $\Gamma_C = \GammaC$
-\end{itemize}
-and thus it enriches the global environment with the following entry:
-\vskip.5em
-\ind{p}{\Gamma_I}{\Gamma_C}
-\vskip.5em
-\noindent that is:
-\vskip.5em
-\ind{0}{\GammaI}{\GammaC}
-\vskip.5em
-\noindent In this case, $\Gamma_P=[~]$.
-
-\vskip1em\hrule\vskip1em
-
-\noindent If we take the following inductive definition:
-\begin{coq_example*}
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \nat & \Set
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r \colon l}
+                        \nO & \nat\\
+                        \nS & \nat\ra\nat
+                      \end{array}
+                \right]}
+    \begin{itemize}
+      \item $p = 0$
+      \item $\Gamma_I = \GammaI$
+      \item $\Gamma_C = \GammaC$
+      \item $\Gamma_P=[\,]$.
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{p}{\Gamma_I}{\Gamma_C}
+    \vskip.5em
+    \noindent that is:
+    \vskip.5em
+    \ind{0}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\nat} inductive type.}
+    \label{fig:nat}
+  \end{figure}
+
+  \begin{figure}[H]
+    \strut If we take the following inductive definition:
+\begin{verbatim}
 Inductive list (A : Type) : Type :=
   | nil : list A
   | cons : A -> list A -> list A.
-\end{coq_example*}
-then:
-\def\GammaI{\left[\begin{array}{r \colon l}
-                    \List & \Type\ra\Type
-                  \end{array}
-            \right]}
-\def\GammaC{\left[\begin{array}{r \colon l}
-                    \Nil & \forall~A\!:\!\Type,~\List~A\\
-                    \cons & \forall~A\!:\!\Type,~A\ra\List~A\ra\List~A
-                  \end{array}
-            \right]}
-\begin{itemize}
-  \item $p = 1$
-  \item $\Gamma_I = \GammaI$
-  \item $\Gamma_C = \GammaC$
-\end{itemize}
-and thus it enriches the global environment with the following entry:
-\vskip.5em
-\ind{p}{\Gamma_I}{\Gamma_C}
-\vskip.5em
-\noindent that is:
-\vskip.5em
-\ind{1}{\GammaI}{\GammaC}
-\vskip.5em
-\noindent In this case, $\Gamma_P=[A:\Type]$.
-
-\vskip1em\hrule\vskip1em
-
-\noindent If we take the following inductive definition:
-\begin{coq_example*}
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \List & \Type\ra\Type
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r \colon l}
+                        \Nil & \forall~A\!:\!\Type,~\List~A\\
+                        \cons & \forall~A\!:\!\Type,~A\ra\List~A\ra\List~A
+                      \end{array}
+                \right]}
+    \begin{itemize}
+      \item $p = 1$
+      \item $\Gamma_I = \GammaI$
+      \item $\Gamma_C = \GammaC$
+      \item $\Gamma_P=[A:\Type]$
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{1}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\List} inductive type.}
+    \label{fig:list}
+  \end{figure}
+
+  \begin{figure}[H]
+    \strut If we take the following inductive definition:
+\begin{verbatim}
 Inductive even : nat -> Prop :=
   | even_O : even 0
   | even_S : forall n, odd n -> even (S n)
 with odd : nat -> Prop :=
   | odd_S : forall n, even n -> odd (S n).
-\end{coq_example*}
-then:
-\def\GammaI{\left[\begin{array}{r \colon l}
-                    \even & \nat\ra\Prop \\
-                    \odd & \nat\ra\Prop
-                  \end{array}
-            \right]}
-\def\GammaC{\left[\begin{array}{r \colon l}
-                    \evenO & \even~\nO \\
-                    \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)
-                  \end{array}
-            \right]}
-\begin{itemize}
-  \item $p = 1$
-  \item $\Gamma_I = \GammaI$
-  \item $\Gamma_C = \GammaC$
-\end{itemize}
-and thus it enriches the global environment with the following entry:
-\vskip.5em
-\ind{p}{\Gamma_I}{\Gamma_C}
-\vskip.5em
-\noindent that is:
-\vskip.5em
-\ind{1}{\GammaI}{\GammaC}
-\vskip.5em
-\noindent In this case, $\Gamma_P=[A:\Type]$.
-
-\vskip1em\hrule\vskip1em
-
-\noindent If we take the following inductive definition:
-\begin{coq_example*}
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \even & \nat\ra\Prop \\
+                        \odd & \nat\ra\Prop
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r \colon l}
+                        \evenO & \even~\nO \\
+                        \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)\\
+                        \oddS & \forall n : \nat, \even~n \ra \odd~(\nS~n)
+                      \end{array}
+                \right]}
+    \begin{itemize}
+      \item $p = 1$
+      \item $\Gamma_I = \GammaI$
+      \item $\Gamma_C = \GammaC$
+      \item $\Gamma_P=[A:\Type]$.
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{1}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\even} and {\odd} inductive types.}
+    \label{fig:even:odd}
+  \end{figure}
+
+  \begin{figure}[H]
+    \strut If we take the following inductive definition:
+\begin{verbatim}
 Inductive has_length (A : Type) : list A -> nat -> Prop :=
   | nil_hl : has_length A (nil A) O
   | cons_hl : forall (a:A) (l:list A) (n:nat),
               has_length A l n -> has_length A (cons A a l) (S n).
-\end{coq_example*}
-then:
-\def\GammaI{\left[\begin{array}{r \colon l}
-                    \haslength & \forall~A\!:\!\Type,~\List~A\ra\nat\ra\Prop
-                  \end{array}
-            \right]}
-\def\GammaC{\left[\begin{array}{r c l}
-                    \nilhl & \hskip.1em:\hskip.1em & \forall~A\!:\!\Type,~\haslength~A~(\Nil~A)~\nO\\
-                    \conshl & \hskip.1em:\hskip.1em & \forall~A\!:\!\Type,~\forall~a\!:\!A,~\forall~l\!:\!\List~A,~\forall~n\!:\!\nat,\\
-                           & & \haslength~A~l~n\ra \haslength~A~(\cons~A~a~l)~(\nS~n)
-                  \end{array}
-            \right]}
-\begin{itemize}
-  \item $p = 1$
-  \item $\Gamma_I = \GammaI$
-  \item $\Gamma_C = \GammaC$
-\end{itemize}
-and thus it enriches the global environment with the following entry:
-\vskip.5em
-\ind{p}{\Gamma_I}{\Gamma_C}
-%\vskip.5em
-%\noindent that is:
-%\vskip.5em
-%\ind{1}{\GammaI}{\GammaC}
-\vskip.5em
-\noindent In this case, $\Gamma_P=[A:\Type]$.
-
-\vskip1em\hrule\vskip1em
-
-\noindent If we take the following inductive definition:
-\begin{coq_example*}
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \haslength & \forall~A\!:\!\Type,~\List~A\ra\nat\ra\Prop
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r c l}
+                        \nilhl & \hskip.1em:\hskip.1em & \forall~A\!:\!\Type,~\haslength~A~(\Nil~A)~\nO\\
+                        \conshl & \hskip.1em:\hskip.1em & \forall~A\!:\!\Type,~\forall~a\!:\!A,~\forall~l\!:\!\List~A,~\forall~n\!:\!\nat,\\
+                               & & \haslength~A~l~n\ra \haslength~A~(\cons~A~a~l)~(\nS~n)
+                      \end{array}
+                \right]}
+    \begin{itemize}
+      \item $p = 1$
+      \item $\Gamma_I = \GammaI$
+      \item $\Gamma_C = \GammaC$
+      \item $\Gamma_P=[A:\Type]$.
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{p}{\Gamma_I}{\Gamma_C}
+    %\vskip.5em
+    %\noindent that is:
+    %\vskip.5em
+    %\ind{1}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\haslength} inductive type.}
+    \label{fig:haslength}
+  \end{figure}
+
+  \begin{figure}[H]
+    \strut If we take the following inductive definition:
+\begin{verbatim}
 Inductive tree : Set :=
   | node : forest -> tree
 with forest : Set :=
   | emptyf : forest
   | consf : tree -> forest -> forest.
-\end{coq_example*}
-then:
-\def\GammaI{\left[\begin{array}{r \colon l}
-                    \tree & \Set\\
-                    \forest & \Set
-                  \end{array}
-            \right]}
-\def\GammaC{\left[\begin{array}{r \colon l}
-                    \node & \forest\ra\tree\\
-                    \emptyf & \forest\\
-                    \consf & \tree\ra\forest\ra\forest
-                  \end{array}
-            \right]}
-\begin{itemize}
-  \item $p = 0$
-  \item $\Gamma_I = \GammaI$
-  \item $\Gamma_C = \GammaC$
-\end{itemize}
-and thus it enriches the global environment with the following entry:
-\vskip.5em
-\ind{p}{\Gamma_I}{\Gamma_C}
-\vskip.5em
-\noindent that is:
-\vskip.5em
-\ind{0}{\GammaI}{\GammaC}
-\vskip.5em
-\noindent In this case, $\Gamma_P=[\,]$.
+\end{verbatim}
+    then:
+    \def\GammaI{\left[\begin{array}{r \colon l}
+                        \tree & \Set\\
+                        \forest & \Set
+                      \end{array}
+                \right]}
+    \def\GammaC{\left[\begin{array}{r \colon l}
+                        \node & \forest\ra\tree\\
+                        \emptyf & \forest\\
+                        \consf & \tree\ra\forest\ra\forest
+                      \end{array}
+                \right]}
+    \begin{itemize}
+      \item $p = 0$
+      \item $\Gamma_I = \GammaI$
+      \item $\Gamma_C = \GammaC$
+    \end{itemize}
+    and thus it enriches the global environment with the following entry:
+    \vskip.5em
+    \ind{0}{\GammaI}{\GammaC}
+    \caption{\captionstrut Formal representation of the {\tree} and {\forest} inductive types.}
+    \label{fig:tree:forest}
+  \end{figure}%
+  \newpage
 \end{latexonly}%
 
 \subsection{Types of inductive objects}
@@ -872,68 +872,77 @@ the type $V$ satisfies the nested positivity condition for $X$
 \end{itemize}
 
 \begin{latexonly}%
-\newcommand\vv{\textSFxi}    % │
-\newcommand\hh{\textSFx}     %   ─
-\newcommand\vh{\textSFviii}  % ├
-\newcommand\hv{\textSFii}    %   └
-\newlength\framecharacterwidth
-\settowidth\framecharacterwidth{\hh}
-\newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
-\newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-\paragraph{Example}~\\
-\vskip-.5em
-\noindent$X$ occurs strictly positively in $A\ra X$\ruleref5\\
-\vv\\
-\vh\hh\ws $X$does not occur in $A$\ruleref3\\
-\vv\\
-\hv\hh\ws $X$ occurs strictly positively in $X$\ruleref4
-\paragraph{Example}~\\
-\vskip-.5em
-\noindent $X$ occurs strictly positively in $X*A$\\
-\vv\\
-\hv\hh $X$ occurs strictly positively in $(\Prod~X~A)$\ruleref6\\
-\ws\ws\vv\\
-\ws\ws\vv\ws\verb|Inductive prod (A B : Type) : Type :=|\\
-\ws\ws\vv\ws\verb|  pair : A -> B -> prod A B.|\\
-\ws\ws\vv\\
-\ws\ws\vh\hh $X$ does not occur in any (real) arguments of $\Prod$ in the original term $(\Prod~X~A)$\\
-\ws\ws\vv\\
-\ws\ws\hv\ws the (instantiated) type $\Prod~X~A$ of constructor $\Pair$,\\
-\ws\ws\ws\ws satisfies the nested positivity condition for $X$\ruleref7\\
-\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\hv\ws $X$ does not occur in any (real) arguments of $(\Prod~X~A)$
-\paragraph{Example}~\\
-\vskip-.5em
-\noindent $X$ occurs strictly positively in $\ListA$\ruleref6\\
-\vv\\
-\vv\ws\verb|Inductive list (A:Type) : Type :=|\\
-\vv\ws\verb$  | nil : list A$\\
-\vv\ws\verb$  | cons : A -> list A -> list A$\\
-\vv\\
-\vh\hh $X$ does not occur in any arguments of $\List$\\
-\vv\\
-\hv\hh\ws Every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $X$\\
-\ws\ws\ws\vv\\
-\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
-\ws\ws\ws\vv\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the nested positivity condition for $X$\\
-\ws\ws\ws\vv\ws\ws because $X$ does not appear in any (real) arguments of the type of that constructor\\
-\ws\ws\ws\vv\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref7\\
-\ws\ws\ws\vv\\
-\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
-\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
-\ws\ws\ws\ws\ws\ws satisfies the nested positivity condition for $X$\ruleref8\\
-\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\Type$\ruleref3\\
-\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $A\ra\ListA\ra\ListA$\ruleref8\\
-\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $A$\ruleref3\\
-\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA\ra\ListA$\ruleref8\\
-\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\ListA$\ruleref3\\
-\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA$\ruleref7
+  \newpage
+  \newcommand\vv{\textSFxi}    % │
+  \newcommand\hh{\textSFx}     %   ─
+  \newcommand\vh{\textSFviii}  % ├
+  \newcommand\hv{\textSFii}    %   └
+  \newlength\framecharacterwidth
+  \settowidth\framecharacterwidth{\hh}
+  \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
+  \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
+  \def\captionstrut{\vbox to 1.5em{}}
+
+  \begin{figure}[H]
+    \ws\strut $X$ occurs strictly positively in $A\ra X$\ruleref5\\
+    \ws\vv\\
+    \ws\vh\hh\ws $X$does not occur in $A$\\
+    \ws\vv\\
+    \ws\hv\hh\ws $X$ occurs strictly positively in $X$\ruleref4
+    \caption{\captionstrut A proof that $X$ occurs strictly positively in $A\ra X$.}
+  \end{figure}
+
+%  \begin{figure}[H]
+%    \strut $X$ occurs strictly positively in $X*A$\\
+%    \vv\\
+%    \hv\hh $X$ occurs strictly positively in $(\Prod~X~A)$\ruleref6\\
+%    \ws\ws\vv\\
+%    \ws\ws\vv\ws\verb|Inductive prod (A B : Type) : Type :=|\\
+%    \ws\ws\vv\ws\verb|  pair : A -> B -> prod A B.|\\
+%    \ws\ws\vv\\
+%    \ws\ws\vh\hh $X$ does not occur in any (real) arguments of $\Prod$ in the original term $(\Prod~X~A)$\\
+%    \ws\ws\vv\\
+%    \ws\ws\hv\hh\ws the (instantiated) type $\Prod~X~A$ of constructor $\Pair$,\\
+%    \ws\ws\ws\ws\ws satisfies the nested positivity condition for $X$\ruleref7\\
+%    \ws\ws\ws\ws\ws\vv\\
+%    \ws\ws\ws\ws\ws\hv\hh\ws $X$ does not occur in any (real) arguments of $(\Prod~X~A)$
+%    \caption{\captionstrut A proof that $X$ occurs strictly positively in $X*A$}
+%  \end{figure}
+
+  \begin{figure}[H]
+    \ws\strut $X$ occurs strictly positively in $\ListA$\ruleref6\\
+    \ws\vv\\
+    \ws\vv\ws\verb|Inductive list (A:Type) : Type :=|\\
+    \ws\vv\ws\verb$  | nil : list A$\\
+    \ws\vv\ws\verb$  | cons : A -> list A -> list A$\\
+    \ws\vv\\
+    \ws\vh\hh $X$ does not occur in any (real) arguments of $\List$\\
+    \ws\vv\\
+    \ws\hv\hh\ws Every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $X$\\
+    \ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the nested positivity condition for $X$\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws because $X$ does not appear in any (real) arguments of the type of that constructor\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref7\\
+    \ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the nested positivity condition for $X$\ruleref8\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\Type$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $A\ra\ListA\ra\ListA$\ruleref8\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $A$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA\ra\ListA$\ruleref8\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\ListA$\ruleref4\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA$\ruleref7
+    \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
+  \end{figure}
+  \newpage
 \end{latexonly}%
 
 \paragraph{Correctness rules.}
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index cb5d2ecb54..dcb98d96b3 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -21,6 +21,10 @@
 \usepackage{multicol}
 \usepackage{xspace}
 \usepackage{pmboxdraw}
+\usepackage{float}
+
+\floatstyle{boxed} 
+\restylefloat{figure}
 
 % for coqide
 \ifpdf   % si on est pas en pdflatex