diff --git a/dev/sidekick/Sidekick_core/Gensym/index.html b/dev/sidekick/Sidekick_core/Gensym/index.html
index 801d871e..f388a636 100644
--- a/dev/sidekick/Sidekick_core/Gensym/index.html
+++ b/dev/sidekick/Sidekick_core/Gensym/index.html
@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Gensym (sidekick.Sidekick_core.Gensym)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> &#x00BB; <a href="../index.html">Sidekick_core</a> &#x00BB; Gensym</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_core.Gensym</span></code></h1><p>Fresh symbol generation</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type" id="type-term" class="anchored"><a href="#type-term" class="anchor"></a><code><span><span class="keyword">type</span> term</span><span> = <a href="../../Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-ty" class="anchored"><a href="#type-ty" class="anchor"></a><code><span><span class="keyword">type</span> ty</span><span> = <a href="../../Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-t" class="anchored"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Fresh symbol generator.</p><p>The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-create" class="anchored"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>New (stateful) generator instance.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-fresh_term" class="anchored"><a href="#val-fresh_term" class="anchor"></a><code><span><span class="keyword">val</span> fresh_term : <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>pre:string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-ty">ty</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-term">term</a></span></code></div><div class="spec-doc"><p>Make a fresh term of the given type</p></div></div></div></body></html>
\ No newline at end of file
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Gensym (sidekick.Sidekick_core.Gensym)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../index.html">sidekick</a> &#x00BB; <a href="../index.html">Sidekick_core</a> &#x00BB; Gensym</nav><header class="odoc-preamble"><h1>Module <code><span>Sidekick_core.Gensym</span></code></h1><p>Fresh symbol generation</p></header><div class="odoc-content"><div class="odoc-spec"><div class="spec type" id="type-term" class="anchored"><a href="#type-term" class="anchor"></a><code><span><span class="keyword">type</span> term</span><span> = <a href="../../Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-ty" class="anchored"><a href="#type-ty" class="anchor"></a><code><span><span class="keyword">type</span> ty</span><span> = <a href="../../Sidekick_core_logic/Term/index.html#type-t">Sidekick_core_logic.Term.t</a></span></code></div></div><div class="odoc-spec"><div class="spec type" id="type-t" class="anchored"><a href="#type-t" class="anchor"></a><code><span><span class="keyword">type</span> t</span></code></div><div class="spec-doc"><p>Fresh symbol generator.</p><p>The theory needs to be able to create new terms with fresh names, to be used as placeholders for complex formulas during Tseitin encoding.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-create" class="anchored"><a href="#val-create" class="anchor"></a><code><span><span class="keyword">val</span> create : <span><a href="../../Sidekick_core_logic/Term/index.html#type-store">Sidekick_core_logic.Term.store</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-t">t</a></span></code></div><div class="spec-doc"><p>New (stateful) generator instance.</p></div></div><div class="odoc-spec"><div class="spec value" id="val-fresh_term" class="anchored"><a href="#val-fresh_term" class="anchor"></a><code><span><span class="keyword">val</span> fresh_term : <span>?opaque_to_cc:bool <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-t">t</a> <span class="arrow">&#45;&gt;</span></span> <span>pre:string <span class="arrow">&#45;&gt;</span></span> <span><a href="#type-ty">ty</a> <span class="arrow">&#45;&gt;</span></span> <a href="#type-term">term</a></span></code></div><div class="spec-doc"><p>Make a fresh term of the given type</p></div></div></div></body></html>
\ No newline at end of file
diff --git a/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html b/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html
index 5047a3e9..5a7d6719 100644
--- a/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html
+++ b/dev/sidekick/Sidekick_core_logic/Const/module-type-DYN_OPS/index.html
@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_OPS (sidekick.Sidekick_core_logic.Const.DYN_OPS)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> &#x00BB; <a href="../../index.html">Sidekick_core_logic</a> &#x00BB; <a href="../index.html">Const</a> &#x00BB; DYN_OPS</nav><header class="odoc-preamble"><h1>Module type <code><span>Const.DYN_OPS</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-pp" class="anchored"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="../index.html#type-view">view</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-equal" class="anchored"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-hash" class="anchored"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div></div></div></body></html>
\ No newline at end of file
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>DYN_OPS (sidekick.Sidekick_core_logic.Const.DYN_OPS)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 2.1.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body class="odoc"><nav class="odoc-nav"><a href="../index.html">Up</a> – <a href="../../../index.html">sidekick</a> &#x00BB; <a href="../../index.html">Sidekick_core_logic</a> &#x00BB; <a href="../index.html">Const</a> &#x00BB; DYN_OPS</nav><header class="odoc-preamble"><h1>Module type <code><span>Const.DYN_OPS</span></code></h1></header><div class="odoc-content"><div class="odoc-spec"><div class="spec value" id="val-pp" class="anchored"><a href="#val-pp" class="anchor"></a><code><span><span class="keyword">val</span> pp : <span><a href="../index.html#type-view">view</a> <span class="xref-unresolved">Sidekick_util</span>.Fmt.printer</span></span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-equal" class="anchored"><a href="#val-equal" class="anchor"></a><code><span><span class="keyword">val</span> equal : <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-hash" class="anchored"><a href="#val-hash" class="anchor"></a><code><span><span class="keyword">val</span> hash : <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> int</span></code></div></div><div class="odoc-spec"><div class="spec value" id="val-opaque_to_cc" class="anchored"><a href="#val-opaque_to_cc" class="anchor"></a><code><span><span class="keyword">val</span> opaque_to_cc : <span><a href="../index.html#type-view">view</a> <span class="arrow">&#45;&gt;</span></span> bool</span></code></div></div></div></body></html>
\ No newline at end of file
