Fix manual, and include Alexandre's typo fixes

4 files changed, 10 insertions, 10 deletions

diff --git a/doc/Makefile b/doc/Makefile
index 981463ca..7afebdf2 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -85,5 +85,5 @@ clean:
 	-rm -f code_riscv.tex
 	-rm -rf code_myreplicatebits/
 	-rm -f code_myreplicatebits.tex
-	-rm *.aux
-	-rm *.log
+	-rm -f *.aux
+	-rm -f *.log
diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail
index 8c3c9458..9334163b 100644
--- a/doc/examples/my_replicate_bits.sail
+++ b/doc/examples/my_replicate_bits.sail
@@ -44,9 +44,9 @@ function my_replicate_bits_2(n, xs) = {
   ys
 }
 
-val cast extz : forall 'n 'm, 'm >= 'n. bits('n) -> bits('m)
+val cast extz : forall 'n 'm, 'm >= 'n. (implicit('m), bits('n)) -> bits('m)
 
-function extz(xs) = zero_extend(xs, 'm)
+function extz(m, xs) = zero_extend(xs, m)
 
 val my_replicate_bits_3 : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm)
 
diff --git a/doc/riscv.tex b/doc/riscv.tex
index 586efdf4..ee0c07e1 100644
--- a/doc/riscv.tex
+++ b/doc/riscv.tex
@@ -61,7 +61,7 @@ register Xs : vector(32, dec, xlen_t)
 
 \sailval{wX}
 \sailfn{wX}
-\sailoverloadHHX
+\sailoverloadIIX
 
 We also give a function \ll{MEMr} for reading memory, this function
 just points at a builtin we have defined elsewhere. Note that
@@ -138,4 +138,4 @@ end execute
 
 The actual code for this example, as well as our more complete
 \riscv\ specification can be found on our github at
-\anonymise{\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}}.
+\anonymise{\url{https://github.com/rems-project/sail-riscv/blob/master/model/riscv_duopod.sail}}.
diff --git a/doc/tutorial.tex b/doc/tutorial.tex
index dcac1c13..9bf47f5b 100644
--- a/doc/tutorial.tex
+++ b/doc/tutorial.tex
@@ -372,7 +372,7 @@ Sail allows numerous ways to match on bitvectors, for example:
 \begin{lstlisting}
 match v {
   0xFF => print("hex match"),
-  0x0000_0001 => print("binary match"),
+  0b0000_0001 => print("binary match"),
   0xF @ v : bits(4) => print("vector concatenation pattern"),
   0xF @ [bitone, _, b1, b0] => print("vector pattern"),
   _ : bits(4) @ v : bits(4) => print("annotated wildcard pattern")
@@ -499,7 +499,7 @@ written
 \end{lstlisting}
 but it would not have type-checked. The reason for this is if a
 mutable variable is declared without a type, Sail will try to infer
-the most specific type from the left hand side of the
+the most specific type from the right hand side of the
 expression. However, in this case Sail will infer the type as
 \ll{int(3)} and will therefore complain when we try to reassign it to
 \ll{2}, as the type \ll{int(2)} is not a subtype of \ll{int(3)}. We
@@ -629,7 +629,7 @@ implicitly dereference registers if that semantics is desired for a
 specific specification that makes heavy use of register references,
 like so:
 \begin{lstlisting}
-val cast auto_reg_deref = "reg_deref" : forall ('a : Type). register('a) -> a effect {rreg}
+val cast auto_reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a effect {rreg}
 \end{lstlisting}
 
 
@@ -687,7 +687,7 @@ the names of its fields.
 \subsubsection{Unions}
 \label{sec:union}
 
-As an example, the \ll{maybe} type \'{a} la Haskell could be defined
+As an example, the \ll{maybe} type \`{a} la Haskell could be defined
 in Sail as follows:
 \begin{lstlisting}
 union maybe ('a : Type) = {