ott-lang · ohad · Jul 13, 2026 · Jul 13, 2026 · Jul 13, 2026
diff --git a/built_doc/top2.html b/built_doc/top2.html
diff --git a/built_doc/top2.pdf b/built_doc/top2.pdf
diff --git a/built_doc/top2.ps b/built_doc/top2.ps
diff --git a/built_doc/top2001.png b/built_doc/top2001.png
diff --git a/built_doc/top2002.png b/built_doc/top2002.png
diff --git a/built_doc/top2003.png b/built_doc/top2003.png
diff --git a/built_doc/top2004.png b/built_doc/top2004.png
diff --git a/built_doc/top2005.png b/built_doc/top2005.png
diff --git a/built_doc/top2006.png b/built_doc/top2006.png
diff --git a/built_doc/top2007.png b/built_doc/top2007.png
diff --git a/built_doc/top2008.png b/built_doc/top2008.png
diff --git a/built_doc/top2009.png b/built_doc/top2009.png
diff --git a/built_doc/top2010.png b/built_doc/top2010.png
diff --git a/built_doc/top2011.png b/built_doc/top2011.png
diff --git a/built_doc/top2012.png b/built_doc/top2012.png
diff --git a/built_doc/top2013.png b/built_doc/top2013.png
diff --git a/built_doc/top2014.png b/built_doc/top2014.png
diff --git a/built_doc/top2015.png b/built_doc/top2015.png
diff --git a/built_doc/top2016.png b/built_doc/top2016.png
diff --git a/built_doc/top2017.png b/built_doc/top2017.png
diff --git a/built_doc/top2018.png b/built_doc/top2018.png
diff --git a/built_doc/top2019.png b/built_doc/top2019.png
diff --git a/built_doc/top2020.png b/built_doc/top2020.png
diff --git a/built_doc/top2021.png b/built_doc/top2021.png
diff --git a/built_doc/top2022.png b/built_doc/top2022.png
diff --git a/built_doc/top2023.png b/built_doc/top2023.png
diff --git a/built_doc/top2024.png b/built_doc/top2024.png
diff --git a/built_doc/top2025.png b/built_doc/top2025.png
diff --git a/built_doc/top2026.png b/built_doc/top2026.png
diff --git a/built_doc/top2027.png b/built_doc/top2027.png
diff --git a/built_doc/top2028.png b/built_doc/top2028.png
diff --git a/built_doc/top2029.png b/built_doc/top2029.png
diff --git a/built_doc/top2030.png b/built_doc/top2030.png
diff --git a/built_doc/top2031.png b/built_doc/top2031.png
diff --git a/built_doc/top2032.png b/built_doc/top2032.png
diff --git a/built_doc/top2033.png b/built_doc/top2033.png
diff --git a/built_doc/top2034.png b/built_doc/top2034.png
diff --git a/built_doc/top2035.png b/built_doc/top2035.png
diff --git a/built_doc/top2036.png b/built_doc/top2036.png
diff --git a/built_doc/top2037.png b/built_doc/top2037.png
diff --git a/doc/top2.mng b/doc/top2.mng
@@ -579,7 +579,7 @@ Grammar rules can include a \mykw{tex} hom specifying how all the
   type\mysym{,} t\mysym{,} s \mysym{::} Typ_ \mysym{::=}  \mysym{\mylb\mylb{}} \mykw{tex} \mybackslash{}mathsf\mylb{}\mysym{[[}type\mysym{]]}\myrb{} \mysym{\myrb\myrb{}} 
         \mysym{|} unit                  \mysym{::}   \mysym{::} unit   
         \mysym{|} type * type'          \mysym{::}   \mysym{::} pair   
-        \mysym{|} type -> type'         \mysym{::}   \mysym{::} fun    
+        \mysym{|} type -> type'         \mysym{::}   \mysym{::} func   
 \end{alltt}
 %Here that \verb+tex+ hom overrides the default typesetting with
 %\verb+\mathsf+.
@@ -1163,7 +1163,7 @@ and metavariables, or, for strictly concrete terms, to restrict to
 just the former  (and also to prohibit symbolic nonterminals).
 
 
-Figure~\mref{a46} combines the \myLaTeX{} and proof assistant
+Figure~\mref{a68} combines the \myLaTeX{} and proof assistant
 annotations of Sections \mref{a51} and \mref{a58}, adding a
 \texttt{\mysym{\mylb\mylb{}} \mykw{lex} alphanum\mysym{\myrb\myrb{}}}
 hom
@@ -1194,7 +1194,7 @@ and
 
 
 
-Figure~\mref{a46} also specifies an OCaml representation type for
+Figure~\mref{a68} also specifies an OCaml representation type for
 variables, with the \mykw{metavar} hom
 \texttt{\mysym{\mylb\mylb{}} \mykw{ocaml} int\mysym{\myrb\myrb{}}}.
 Executing