Deploying to gh-pages from @ 78d8c2c 🚀

stlc.html

@@ -128,12 +128,12 @@ <h1>stlc.html</h1>
 <div class='clause' predicate='coq.env.const-primitive?'><div class='loc'>File "coq-builtin.elpi", line 754, column 3, character 30933:</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='12'>C</span></div></div><div class='concl'><div class='compound'>coq.env.const-primitive? <span class='name' varname='12'>C</span></div></div></div>
 <div class='clause' predicate='coq.env.begin-module'><div class='loc'>File "coq-builtin.elpi", line 835, column 0, character 34271:</div><div class='hyps'>coq.env.begin-module-functor <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module <span class='name' varname='13'>Name</span> <span class='name' varname='14'>MP</span></div></div></div>
 <div class='clause' predicate='coq.env.begin-module-type'><div class='loc'>File "coq-builtin.elpi", line 848, column 0, character 34752:</div><div class='hyps'>coq.env.begin-module-type-functor <span class='name' varname='15'>Name</span> []</div><div class='concl'><div class='compound'>coq.env.begin-module-type <span class='name' varname='15'>Name</span></div></div></div>
-<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1205, column 0, character 48653:</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='16'>I</span> <span class='name' varname='17'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div></div>
-<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1508, column 0, character 61426:</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='18'>T</span> <span class='name' varname='19'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div></div>
-<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1515, column 0, character 61704:</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='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div></div>
-<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1522, column 0, character 61938:</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='23'>X</span> <span class='name' varname='24'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div></div>
-<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1639, column 0, character 66449:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div></div></div>
-<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1740, column 0, character 70195:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='29'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <span class='name' varname='29'>C</span></div></div></div>
+<div class='clause' predicate='coq.CS.canonical-projections'><div class='loc'>File "coq-builtin.elpi", line 1211, column 0, character 48987:</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='16'>I</span> <span class='name' varname='17'>L</span></div></div><div class='concl'><div class='compound'>coq.CS.canonical-projections <span class='name' varname='16'>I</span> <span class='name' varname='17'>L</span></div></div></div>
+<div class='clause' predicate='coq.reduction.cbv.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1514, column 0, character 61760:</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='18'>T</span> <span class='name' varname='19'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.cbv.whd_all <span class='name' varname='18'>T</span> <span class='name' varname='19'>R</span></div></div></div>
+<div class='clause' predicate='coq.reduction.vm.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1521, column 0, character 62038:</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='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div><div class='concl'><div class='compound'>coq.reduction.vm.whd_all <span class='name' varname='20'>T</span> <span class='name' varname='21'>TY</span> <span class='name' varname='22'>R</span></div></div></div>
+<div class='clause' predicate='coq.reduction.lazy.whd_all'><div class='loc'>File "coq-builtin.elpi", line 1528, column 0, character 62272:</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='23'>X</span> <span class='name' varname='24'>Y</span></div></div><div class='concl'><div class='compound'>coq.reduction.lazy.whd_all <span class='name' varname='23'>X</span> <span class='name' varname='24'>Y</span></div></div></div>
+<div class='clause' predicate='coq.id->name'><div class='loc'>File "coq-builtin.elpi", line 1645, column 0, character 66783:</div><div class='hyps'>coq.string-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div><div class='concl'><div class='compound'>coq.id-&gt;name <span class='name' varname='25'>S</span> <span class='name' varname='26'>N</span></div></div></div>
+<div class='clause' predicate='coq.elpi.accumulate'><div class='loc'>File "coq-builtin.elpi", line 1746, column 0, character 70529:</div><div class='hyps'>coq.elpi.accumulate-clauses <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <div class='compound' level='99'><b>[</b><div class='compound'><span class='name' varname='29'>C</span></div><b>]</b></div></div><div class='concl'><div class='compound'>coq.elpi.accumulate <span class='name' varname='27'>S</span> <span class='name' varname='28'>N</span> <span class='name' varname='29'>C</span></div></div></div>
 <div class='clause' predicate='true'><div class='loc'>File "elpi-builtin.elpi", line 9, column 0, character 89:</div><div class='hyps'><div class='hyp'></div></div><div class='concl'>true</div></div>
 <div class='clause' predicate=';'><div class='loc'>File "elpi-builtin.elpi", line 28, column 0, character 296:</div><div class='hyps'><span class='name' varname='30'>A</span></div><div class='concl'><div class='compound'><div class='compound'>(<span class='name' varname='30'>A</span>&nbsp;;&nbsp;</div><div class='compound'>_)</div></div></div></div>
 <div class='clause' predicate=';'><div class='loc'>File "elpi-builtin.elpi", line 30, column 0, character 311:</div><div class='hyps'><span class='name' varname='31'>B</span></div><div class='concl'><div class='compound'><div class='compound'>(_&nbsp;;&nbsp;</div><div class='compound'><span class='name' varname='31'>B</span>)</div></div></div></div>