code mort dans tactinterp; plus de Debug On/Off dans Correctness

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2490 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 1 deletions

diff --git a/theories/IntMap/Adist.v b/theories/IntMap/Adist.v
index 5c3296885..fbc2870f1 100644
--- a/theories/IntMap/Adist.v
+++ b/theories/IntMap/Adist.v
@@ -270,7 +270,7 @@ Qed.
     d(a,a'')+d(a'',a')$,
   but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$.
   This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [ad_pdist_ultra] below).
-  This follows from the fact that $a \Ra |a| = 1/2^{\texttt{ad\_plength}}(a))$
+  This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{ad\_plength}}(a))$
   is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$,
   or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that
   min $(\texttt{ad\_plength}(a), \texttt{ad\_plength}(b)) \leq