Pretty printing error on nameless pi bindings fixed

darcs-hash:20060802100604-974a0-3168862fc9a9f6ed61600a7a1cfab1a73b14cc20.gz

Ivor/TTCore.lhs

@@ -565,7 +565,7 @@ Apply a function to a list of arguments
 >       fPrec x (RBind n (B Pi t) sc) 
 >           | nameOccurs n sc = bracket x 2 $
 >              "("++forget n ++":"++fPrec 10 t++") -> " ++ fPrec 10 sc
->           | otherwise = bracket x 2
+>           | otherwise = bracket x 2 $
 >              (fPrec 1 t) ++" -> " ++ fPrec 10 sc
 >       fPrec x (RBind n (B (Let v) t) sc) = bracket x 2 $
 >           "let "++forget n ++":"++ fPrec 10 t

papers/ivor/corett.tex

@@ -36,7 +36,9 @@ \subsection{The Core Calculus}
 functional programming languages, we may also write the function space
 \mbox{$\all{\vx}{\vS}\SC\vT$} as \mbox{$\fbind{\vx}{\vS}{\vT}$}, or
 abbreviate it to \mbox{$\vS\to\vT$} if $\vx$ is not free in
-$\vT$. Contexts ($\Gamma$) are defined inductively; the empty context
+$\vT$. 
+Universe levels on types ($\Type_i$) may be left implicit.
+Contexts ($\Gamma$) are defined inductively; the empty context
 is valid, as is a context extended with a $\lambda$, $\forall$ or
 $\LET$ binding:
 

papers/ivor/ivor.tex

@@ -70,7 +70,8 @@
 
 \section*{Acknowledgements}
 
-This work is generously supported by EPSRC grant EP/C001346/1.
+This work is generously supported by EPSRC grant EP/C001346/1. My thanks to
+\ldots
 
 \bibliographystyle{abbrv}
 \begin{small}

papers/ivor/tactics.tex

@@ -121,7 +121,7 @@ \subsection{Basic Tactics}
 
 A tactic operates on a hole binding, specified by the \texttt{Goal}
 argument. This can be a named binding, \texttt{goal :: Name -> Goal},
-or the default goal \texttt{defaultGoal::Name}. The default goal is
+or the default goal \texttt{defaultGoal :: Goal}. The default goal is
 the first goal generated by the most recent tactic application.
 
 \mysubsubsection{Hole Manipulations}