Deploying to gh-pages from @ a7b9cfb 🚀

stlc.html

@@ -369,12 +369,12 @@ <h1>/home/runner/work/coq-elpi/coq-elpi/_build/default/examples/stlc.html</h1>
 <div class='clause' predicate='coq.env.const-primitive?'><div class='loc'>File "coq-builtin.elpi", line 757, column 3, character 31020:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.const-primitive use coq.env.primitive? in place of coq.env.const-primitive?,</div><div class='hyp compound'>coq.env.primitive? <span class='name' varname='717'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-primitive? <span class='name' varname='717'>C</span></div></div></div>
 <div class='clause' predicate='coq.env.begin-module'><div class='loc'>File "coq-builtin.elpi", line 839, column 0, character 34362:</div><div class='hyps'>coq.env.begin-module-functor <span class='name' varname='718'>Name</span> <span class='name' varname='719'>MP</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module <span class='name' varname='718'>Name</span> <span class='name' varname='719'>MP</span></div></div></div>
 <div class='clause' predicate='coq.env.begin-module-type'><div class='loc'>File "coq-builtin.elpi", line 852, column 0, character 34843:</div><div class='hyps'>coq.env.begin-module-type-functor <span class='name' varname='720'>Name</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module-type <span class='name' varname='720'>Name</span></div></div></div>
-<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1236, column 0, character 49945:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,</div><div class='hyp compound'>coq.env.projections <span class='name' varname='721'>I</span> <span class='name' varname='722'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='721'>I</span> <span class='name' varname='722'>L</span></div></div></div>
-<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1540, column 0, character 62751:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,</div><div class='hyp compound'>coq.reduction.cbv.norm <span class='name' varname='723'>T</span> <span class='name' varname='724'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='723'>T</span> <span class='name' varname='724'>R</span></div></div></div>
-<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1547, column 0, character 63029:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,</div><div class='hyp compound'>coq.reduction.vm.norm <span class='name' varname='725'>T</span> <span class='name' varname='726'>TY</span> <span class='name' varname='727'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='725'>T</span> <span class='name' varname='726'>TY</span> <span class='name' varname='727'>R</span></div></div></div>
-<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1554, column 0, character 63263:</div><div class='hyps'><div class='compound'>get-option coq:redflags coq.redflags.all&nbsp;<b>⇒</b>&nbsp;</div><div class='compound'>coq.reduction.lazy.whd <span class='name' varname='728'>X</span> <span class='name' varname='729'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='728'>X</span> <span class='name' varname='729'>Y</span></div></div></div>
-<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1671, column 0, character 67774:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='730'>S</span> <span class='name' varname='731'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='730'>S</span> <span class='name' varname='731'>N</span></div></div></div>
-<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1773, column 0, character 71548:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='732'>S</span> <span class='name' varname='733'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='734'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='732'>S</span> <span class='name' varname='733'>N</span> <span class='name' varname='734'>C</span></div></div></div>
+<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1231, column 0, character 49739:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.canonical-projections use coq.env.projections in place of coq.CS.canonical-projections,</div><div class='hyp compound'>coq.env.projections <span class='name' varname='721'>I</span> <span class='name' varname='722'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='721'>I</span> <span class='name' varname='722'>L</span></div></div></div>
+<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1535, column 0, character 62545:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.cbv-whd-all use coq.reduction.cbv.norm in place of coq.reduction.cbv.whd_all,</div><div class='hyp compound'>coq.reduction.cbv.norm <span class='name' varname='723'>T</span> <span class='name' varname='724'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='723'>T</span> <span class='name' varname='724'>R</span></div></div></div>
+<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1542, column 0, character 62823:</div><div class='hyps'><div class='hyp compound' level='60'>coq.warning elpi.deprecated elpi.vm-whd-all use coq.reduction.vm.norm in place of coq.reduction.vm.whd_all,</div><div class='hyp compound'>coq.reduction.vm.norm <span class='name' varname='725'>T</span> <span class='name' varname='726'>TY</span> <span class='name' varname='727'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='725'>T</span> <span class='name' varname='726'>TY</span> <span class='name' varname='727'>R</span></div></div></div>
+<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1549, column 0, character 63057:</div><div class='hyps'><div class='compound'>get-option coq:redflags coq.redflags.all&nbsp;<b>⇒</b>&nbsp;</div><div class='compound'>coq.reduction.lazy.whd <span class='name' varname='728'>X</span> <span class='name' varname='729'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='728'>X</span> <span class='name' varname='729'>Y</span></div></div></div>
+<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1666, column 0, character 67568:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='730'>S</span> <span class='name' varname='731'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='730'>S</span> <span class='name' varname='731'>N</span></div></div></div>
+<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1768, column 0, character 71342:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='732'>S</span> <span class='name' varname='733'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='734'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='732'>S</span> <span class='name' varname='733'>N</span> <span class='name' varname='734'>C</span></div></div></div>
 <div class='clause' predicate='whd'><div class='loc'>File "./examples/tutorial_elpi_lang.v", line 491, column 3, character 12653:</div><div class='hyps'><div class='hyp compound' level='60'>whd <span class='name' varname='735'>Hd</span> (fun <span class='name' varname='738'>F</span>),</div><div class='hyp compound'><span class='cut'>!</span>,</div><div class='hyp compound'>whd (<span class='name' varname='738'>F</span> <span class='name' varname='736'>Arg</span>) <span class='name' varname='737'>Reduct</span></div></div><div class='concl'><div class='compound'>whd (app <span class='name' varname='735'>Hd</span> <span class='name' varname='736'>Arg</span>) <span class='name' varname='737'>Reduct</span></div></div></div>
 <div class='clause' predicate='whd'><div class='loc'>File "./examples/tutorial_elpi_lang.v", line 495, column 3, character 12776:</div><div class='hyps'><div class='compound'><span class='name' varname='740'>Reduct</span>&nbsp;=&nbsp;</div><div class='compound'><span class='name' varname='739'>X</span></div></div><div class='concl'><div class='compound'>whd <span class='name' varname='739'>X</span> <span class='name' varname='740'>Reduct</span></div></div></div>
 <div class='clause' predicate='of'><div class='loc'>File "./examples/tutorial_elpi_lang.v", line 591, column 3, character 15201:</div><div class='hyps'><div class='hyp compound' level='60'>of <span class='name' varname='741'>Hd</span> (arr <span class='name' varname='744'>A</span> <span class='name' varname='743'>B</span>),</div><div class='hyp compound'>of <span class='name' varname='742'>Arg</span> <span class='name' varname='744'>A</span></div></div><div class='concl'><div class='compound'>of (app <span class='name' varname='741'>Hd</span> <span class='name' varname='742'>Arg</span>) <span class='name' varname='743'>B</span></div></div></div>