@@ -218,9 +218,9 @@ above to an environment that already is the result of $\Refinef$, and so on. The

algorithm should compute the type environment as a fixpoint of the

function $X\mapsto\Refine{e,t}{X}$. Unfortunately, an iteration of $\Refinef$ may

not converge. As an example, consider the (dumb) expression $\tcase

{x x}{\Any}{e_1}{e_2}$. If $x:\Any\to\Any$, then every iteration of

{x x}{\Any}{e_1}{e_2}$. If $x:\Any\to\Any$, then when refining the ``then'' branch, every iteration of

$\Refinef$ yields for $x$ a type strictly more precise than the type deduced in the

previous iteration.

previous iteration (because of the $\varpi.0$ case).

The solution we adopt in practice is to bound the number of iterations to some number $n_o$. This is obtained by the following definition of $\Refinef$\svvspace{-1mm}