[github pages] BRiCk documentation created from 3f842dd

docs/_static/coqdoc/bedrock.lang.cpp.logic.wp.html

@@ -1215,6 +1215,8 @@ <h1 class="libtitle">bedrock.lang.cpp.logic.wp</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">c</span> =&gt; <a class="idref" href="bedrock.lang.cpp.logic.wp.html#Q:517"><span class="id" title="variable">Q</span></a> <span class="id" title="var">c</span> <a class="idref" href="bedrock.lang.cpp.logic.wp.html#free:519"><span class="id" title="variable">free</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> =&gt; <a class="idref" href="bedrock.lang.bi.errors.html#Errors.ERROR"><span class="id" title="abbreviation">ERROR</span></a> (<a class="idref" href="bedrock.lang.cpp.semantics.values.html#VALUES_INTF_AXIOM.is_true_None"><span class="id" title="record">is_true_None</span></a> <a class="idref" href="bedrock.lang.cpp.logic.wp.html#v:518"><span class="id" title="variable">v</span></a>)<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>).<br/>
+&nbsp;&nbsp;#[<span class="id" title="var">global</span>] <span class="id" title="keyword">Hint</span> <span class="id" title="keyword">Opaque</span> <a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.wp_test"><span class="id" title="definition">wp_test</span></a> : <span class="id" title="var">br_opacity</span>.<br/>
+&nbsp;&nbsp;#[<span class="id" title="var">global</span>] <span class="id" title="var">Arguments</span> <a class="idref" href="bedrock.lang.cpp.logic.wp.html#WPE.wp_test"><span class="id" title="definition">wp_test</span></a> /.<br/>
 
 <br/>
 &nbsp;&nbsp;<span class="id" title="keyword">Lemma</span> <a id="WPE.wp_test_frame" class="idref" href="#WPE.wp_test_frame"><span class="id" title="lemma">wp_test_frame</span></a> {<a id="9ca2482234ee9bc565f41cdd52c4565d" class="idref" href="#9ca2482234ee9bc565f41cdd52c4565d"><span class="id" title="binder">σ</span></a> : <a class="idref" href="bedrock.lang.cpp.semantics.genv.html#genv"><span class="id" title="class">genv</span></a>} <a id="tu:521" class="idref" href="#tu:521"><span class="id" title="binder">tu</span></a> <a id="368814e4482476efecddd85a0fbcd2a4" class="idref" href="#368814e4482476efecddd85a0fbcd2a4"><span class="id" title="binder">ρ</span></a> <a id="test:523" class="idref" href="#test:523"><span class="id" title="binder">test</span></a> (<a id="Q:524" class="idref" href="#Q:524"><span class="id" title="binder">Q</span></a> <a id="Q':525" class="idref" href="#Q':525"><span class="id" title="binder">Q'</span></a> : <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.18.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="bedrock.lang.cpp.logic.wp.html#epred"><span class="id" title="definition">epred</span></a>) :<br/>