From 1a17d4ec43a0744dd2bd20a9673eee37d0cbaf9c Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 13 Jul 2026 06:36:50 +0100 Subject: [PATCH 1/3] Manual: fix syntax error using 'fun' in the comment throws a syntax error, rename to 'func' --- doc/top2.mng | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/top2.mng b/doc/top2.mng index b243dd3..fcd42aa 100644 --- 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+. From 712dc96a1686405510a14a2db3f78e5b4af75458 Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 13 Jul 2026 06:37:54 +0100 Subject: [PATCH 2/3] Manual: fix cross-refs in sec. 7 (concrete terms and OCaml gen.) I think the prose should refer to figure 8 (a68) rather than figure 2 (a46) --- doc/top2.mng | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/top2.mng b/doc/top2.mng index fcd42aa..6d0e3c6 100644 --- a/doc/top2.mng +++ b/doc/top2.mng @@ -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 From 752e6c74135e5253d84bdd98ecc249e3312b5cae Mon Sep 17 00:00:00 2001 From: Ohad Kammar Date: Mon, 13 Jul 2026 06:44:31 +0100 Subject: [PATCH 3/3] Rebuild the docs --- built_doc/top2.html | 1961 +++++++++++++++++++++-------------------- built_doc/top2.pdf | Bin 542711 -> 542829 bytes built_doc/top2.ps | Bin 3014872 -> 3014865 bytes built_doc/top2001.png | Bin 5024 -> 5024 bytes built_doc/top2002.png | Bin 796 -> 796 bytes built_doc/top2003.png | Bin 753 -> 753 bytes built_doc/top2004.png | Bin 482 -> 482 bytes built_doc/top2005.png | Bin 2185 -> 2185 bytes built_doc/top2006.png | Bin 1290 -> 1290 bytes built_doc/top2007.png | Bin 20905 -> 20905 bytes built_doc/top2008.png | Bin 904 -> 904 bytes built_doc/top2009.png | Bin 725 -> 725 bytes built_doc/top2010.png | Bin 391 -> 391 bytes built_doc/top2011.png | Bin 340 -> 340 bytes built_doc/top2012.png | Bin 1094 -> 1094 bytes built_doc/top2013.png | Bin 600 -> 600 bytes built_doc/top2014.png | Bin 352 -> 352 bytes built_doc/top2015.png | Bin 353 -> 353 bytes built_doc/top2016.png | Bin 2975 -> 2975 bytes built_doc/top2017.png | Bin 352 -> 352 bytes built_doc/top2018.png | Bin 382 -> 382 bytes built_doc/top2019.png | Bin 9794 -> 9794 bytes built_doc/top2020.png | Bin 1185 -> 1185 bytes built_doc/top2021.png | Bin 444 -> 444 bytes built_doc/top2022.png | Bin 477 -> 477 bytes built_doc/top2023.png | Bin 5983 -> 5983 bytes built_doc/top2024.png | Bin 4246 -> 4246 bytes built_doc/top2025.png | Bin 1543 -> 1543 bytes built_doc/top2026.png | Bin 1202 -> 1202 bytes built_doc/top2027.png | Bin 2133 -> 2133 bytes built_doc/top2028.png | Bin 2447 -> 2447 bytes built_doc/top2029.png | Bin 3922 -> 3922 bytes built_doc/top2030.png | Bin 2957 -> 2957 bytes built_doc/top2031.png | Bin 575 -> 575 bytes built_doc/top2032.png | Bin 355 -> 355 bytes built_doc/top2033.png | Bin 374 -> 374 bytes built_doc/top2034.png | Bin 1637 -> 1637 bytes built_doc/top2035.png | Bin 2049 -> 2049 bytes built_doc/top2036.png | Bin 1207 -> 1207 bytes built_doc/top2037.png | Bin 3116 -> 3116 bytes 40 files changed, 1003 insertions(+), 958 deletions(-) diff --git a/built_doc/top2.html b/built_doc/top2.html index b47fd2b..767ba3c 100644 --- a/built_doc/top2.html +++ b/built_doc/top2.html @@ -2,7 +2,7 @@ - +