From 9bdda2beaa7b0f836e3700a2e2458761e8eee06d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Mon, 7 Dec 2020 20:44:36 +0100 Subject: [PATCH] =?utf8?q?=CE=BB=CE=B4=20site=20update?= MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit + another Unicode character sponsored + Helena: minor updates + Ground: minor updates --- helm/software/helena/src/common/layer.ml | 2 +- helm/software/helena/src/toplevel/helena.ml | 2 +- helm/www/lambdadelta/images/bronze-03C7.png | Bin 0 -> 12241 bytes helm/www/lambdadelta/web/home/home.ldw.xml | 1 + .../contribs/lambdadelta/ground/lib/exteq.ma | 1 - 5 files changed, 3 insertions(+), 3 deletions(-) create mode 100644 helm/www/lambdadelta/images/bronze-03C7.png diff --git a/helm/software/helena/src/common/layer.ml b/helm/software/helena/src/common/layer.ml index 82300931b..c0b6bcc19 100644 --- a/helm/software/helena/src/common/layer.ml +++ b/helm/software/helena/src/common/layer.ml @@ -39,7 +39,7 @@ let warn s = L.warn (pred level) s let zero = Fin 0 let string_of_value k = function - | Inf -> "" + | Inf -> "-" | Fin i -> string_of_int i | Ref (k, i) -> "-" ^ P.string_of_mark k ^ "-" ^ string_of_int i | Unk -> "-" ^ P.string_of_mark k diff --git a/helm/software/helena/src/toplevel/helena.ml b/helm/software/helena/src/toplevel/helena.ml index 63a8c0621..10c9f0f7f 100644 --- a/helm/software/helena/src/toplevel/helena.ml +++ b/helm/software/helena/src/toplevel/helena.ml @@ -386,7 +386,7 @@ END IFDEF MANAGER THEN -let set_manager s = match KS.lowercase s with +let set_manager s = match KS.lowercase_ascii s with | "v8" -> G.manager := G.Coq | "ma2" -> G.manager := G.Matita | "lp1" -> G.manager := G.LP1 diff --git a/helm/www/lambdadelta/images/bronze-03C7.png b/helm/www/lambdadelta/images/bronze-03C7.png new file mode 100644 index 0000000000000000000000000000000000000000..f33b0a8fedb2f26b621062a3d4a4c2549b229c43 GIT binary patch literal 12241 zcmV;?FD}rDP)004R>004l5008;`004mK004C`008P>0026e000+ooVrmw0004W zP)t-s|Ns9?X>kS!2*ZF@*OO)2mucUdZQh$~;GAvUnQG#naH35v1qTNZ3kuVUUB`V= zqE|D&a7C|TI|v8}1P2Gda6||Q2*PwopH3@dF&qsF36w-6uv;^tODLd5CFiDf+m&b5 zk73e?TgG=w&VyCNbxF8mJG5Ols!uSaMI_>&aLj;Hyl6kLS2U+eEYyo$zH33`qjT7j zWWaAktWq(;az@aGSl^p$-I!^tVL!QWO2~Rmy?s`HDHzFxTgrV^z_7%eEIV3qE0Wna!=p5qtBFcpP!##U|>K%K(DW_&(F^wARqt$ z0PpYb-{0R55D+jhFi=oXzrVkKe}9jUkIRT-aBy(jtdW2|C-&&x^4Q1Mlxpa%pX>Ml9p2gypAv?4Fog0000VbW%=J0006SH(z|7z0&Fa1`Fzy z3j!-NwUC&W001o-NklLz(uEf_$PLngtf5X}d^>sJAHRbba{++-Sw*<4;$)@PU^=W|(+>38$SwM&M(3b2(M zH{S(s3t}celjs;=UHxJ>0P9qif-jJ`s#q^6uN%W^3PrfCp`B8Fo{meX`< zsfciIgK+;}f&taW#)e)^pa4kIqy7ZT3WW`B)b9W=fvf5;`?AAeY3{IVE~#AaP`I(Ox79= zoUdscDJw`3oPoN%d+}UyNnqDNtXh%#mTw9Lj_vzDi%fcSG zvr~hGFh7FaXh-UGi;S&Y6*e|5hIR>Hh^19n95sa~whH8Wp-mWtw%G0R(B#W?9VUgH z9lg*6cp(l-p~<4TqFoH_!eG~K0)tJyV9zJN8>>tcJ)H&%-N>N3;hPrVpxpwzf@U@N z9IZsf*;=8nJlX}puD$gx$Li&TC<6l07D^^W;&qcGKb0|}**dmBqt)V*g$*Is<7n@` zwItewz*cU&TM+tXFe6t(Hw)Vq^r*t>Dked0oQ>d~PJQ%xj5&#T#S{8*`%J?J#)N0*iX?it=4YM|^mPIWDGm3;( ztry;2X1}&P*veboZc%}%m0S%SYhzP4toBAB<$S7Jkvzm!t8vC|ijPliS=%tW-G)^Q zwHy^+>~`N;T(qUZuD{b2ZEDgQI)|x^GGCVu(0>?Bqj6QIzJm7_|9F139Zc2)J*Pabn55cfYFhisKdwRoGDQ{2HuBGakya*K<$9N4vY zYNCT-l0^ooA>pvj5gAOZLIlvQ)w$K`d=Ab`#OfwQ?K@bl1>$Nz? zu$Ev@42UWy!jKx$&=v{Dg~6_~Ff=+;d#lx8;ZtYM)LDbqBN1wT;QPU_Ti6YD3*FGK z*Y^OY26MXIz1=X_?bdwX+hdW7oshzi716~eT5au6IUR$Ah)o;*DZL##>RFq4B(9`?c;}tX4td%a#o;3&NM*rnJlKk$aZeyuhPc6S4>R@;XF6ubZx+Z%Yn zur3Jufd|{{!dmTZ2GWgy;sP0Gy^Y~mfr@3JK4;!v1Z-vHW?fUE_zuEYtu5vQBN7-P z_oeOyZ86xb)u1N@LAwTBYb0o)FCZ9(ATAl<*2BQ}c3}%asI&b6*Q%aEYqTt!=s?w~ zR>u@_KH5THz-1_kVN(4&twzKJxj}$88zU7#2tN!5+qHJ!5kYr|Gawo6LQML>UTr%J zNhjYQ`ul9}whbL}k4RW?yzII#hMhl7nOHj`yG$_P%0kJG#;WUV=`{iYmjr=Pwc9Z! z__!U8;Bx??P|SHlSSqylG+}SphCl@K>LM*;HVTG=a64+H8hc~G;ufz{Q-Lfy7unok zE7#r;I*Ovmx=`0U8W)J_6$Ank1dvDIjSOCjZ2%JnkO_C&f}n$Oe6}GV4tFu>kM?0P z&KL#T;y#S-vC??yQ8n$pUKey3T<8dIUpqG%=LK6?c{}E+uePi@C*oY(kwGBBh>kP% z0|=~bT&U|)JOb}I+_v{e;T~%mj86E3uDH)j6jJY<)>uf$Zk;FE++a6}t3tJmTdM-o ziGRQlT@vSc^l99p zLS#2@-?|hq)4~*x5 zz8CD*IU0Vj#u54Y6>tQ|&XH^`Fv#;l5xJmPvn|ZB5O!RWj{Bxz=%wcKj+IC^b8Cv; z{SdN=4&m%+`@z1>Ho*mYJz7QBk~mpWI4A4R2lkdOshq3TDsqSQs5Ufj0G$e?^1-=w zw17n&%EhL{*z`Cc6XgVPZx4m@0Wg#VeRsH<(6JYu&B7;;sgi#7o_Zdzl^et*W94lC zL#PzjKGd)82kilp?GLvjAaaSE*LC3(q2m6gvqA-Z5Nx;i_ccKq!0uqcrDE0TLZ-E& z;gn2dXP(B)19tsA(J>60HFLYjoQdf)$Yr{|9fYA5gl(FgSmZs4ROd&^bix)dPklmX z)VKGk1V|yC1P7Bk$Ku7dH5wId!*Im+&N?EV1MJ#+I+eqD^zDGmqUDP?E$Ue8BP+boPDfy`#`D)bC`g_+-Cp#Z(Mdt~11du>r! z#bSp`5h(&6yQr8r+>Q56qDI4dVPnJ0bEp|iDLM|9H#as4LfkMKFAjs<3-;Rno*vb} z8h2|8R1`nM@Fnxj=Yf^*Ug9@%qBY%Y~{LWs;b(AqMEIp zte7&`ZvojJ93%vOTZ`3#AjE6#*s=cl=^Rv??NjV>UcRBQKoiky%+Fm$SuG2ORaNb4Z_kkIbg-2h8gx!aqB6EpB|?(ghVx?> z+uxHkont{53Lw|vr^{oZeR_zurfLF}DRGeDE}VU8-frBAIOw;=Fq9lfZra_GWT%3` zu33^Dr>RLPCRXGy2nP^_SgZ!^D$z*2CK(WgOLVT2@n}f3I>iDf3rBDgBVjF5nvr!J zN0#2ZcOn>12YXAZI!=EE7bq15Ly1+y7E5Bij`smCC>IwE@ATE{BCi47!(a$eqG{94 zaO*oxRXUkJP6GqMvX0|qHLc0vs2)k%9<((H_FwzcTzCQcBE4(6r_n`pQH#kuNR7}3 zhTc9+N)oHrY(N(=(arbXKTdWk*d3_^O`%C}$gw5y;&3ns+c3Ee2Llq#qJ2souZlgJ zdxw0U{p}fE=SyqW-qs|%CIVe8YEYnq(+&89z$!_1<^)^0CSmZJl9b(PWmqxPQo~?Z z8iHo+T{evaQILS^i_5}7`vS;BK{R=DV*R^8xQ|zPShdv1Tdf@!F(DOnq~nsE26jh+ z*xkhKvmJ>WlnDEiZD0dn$<+94;4&2DQo2`SpDKzW31U<)*oa~z@OUdHW^O_*knY@{ z2Mh(1W!pSff@GRQytYAH(LCUC73H(bA$Q8Ia~(C79bfW&O_ zY13>pc`qxzcP~vg6YNH|N`j>fCbojXt``QoY%+_BHGR`CE;Y|j+ZTqhsf&pVW(RiF zBS<5O3(P>WYWD6qU@N!YqZUYWnOQSC4B&Gw9N+}LfJ@A}?z5}oIyiXdx>-@<)j>|i z`xfSIuxB1~jw0;6`zf+nVAr!5+pd~s(d}omR3;3wkm+|}d=y5tKp<+4`}a#b-k4>7 z`@8FC6pU2qez-pj_C1Ok?nO4+u$pGJV%wQ1$!3Aw$@Xo#lQqY!9n^-CnOk8vY;J*K z1Pik@G4HyUbbNT4eeSw>kSv>JZZu8GjU0;&S}iwgHf_6~y>tKe8DNk)I2L#*QC2v^c!qBj`U<$Qpr_#p^ zu)Eo+ZRfJg`zh-T2g9vs!i3{$^-4P!vuCPfYOybaK{oQt%%*+JLGQ`ly?+MSEsDfq z_B@lczUo}~yz+c|?x-b@jN8_3%7t{(7cmw;g!FM5*vhpc#A}7ET+B`brlw4-={Q#& zh-hEpdHgA@n{o)!N3*yV$Kpw_yTxigpUGy`RwLmmvcGsn5suJo=kI?6*TKQx9b1yp zD96KTwPj?pnS8!lOk(jQ*qvfOp9cb~Wfg%0OW_|898E|$$GPH+7}@8Jlata;6tm4V z9J&fK^Z9=9!#FP<2V1#SZ07S7*sQWzEhaR`SY*1=~T$nnl*c>|-$4 zEylr9%osUX0)f^n#(D7s7)4^PIAyTa?qF+bjsyoWe?aEolHmbfmV1I+4LATPGR`7z z_F^$N6^qBfRv;2f`Fy8%%yy}yVu!zrCLDBK;W6TI`vMQiQ|@eyg015&7CZTTsfhdN zm04i7KI&j3!nRFD*I^`s(BoVke3_X)P%udOaMo+4-RWe=lQ^JqC74D)_xkISf@FV(V}@ev$T2H+ntlB2_bZ({{M_X@ z*hfuVdXC}o%e)62-~Qt}vKQY^&*!s$n6sEK;VAC}Q|{O_Xwr;2*>SKA=(%|YQxh8q zk2vQ%4g2=xcieuQBKw-n{AOOo{)Wfp$9x$LkImS`UUcvNEU@=k4{UCh7(e&}m~Jv3Gb+Rx<~`_Sw@-kr-1?wd zEtO!+otDd3V8hPP4}5R96~o~kW6ldx|NULceop59%;R%zu7l5T@7j!-ISldpgH7&W zhb6marc|mnKVY5g7}%X=1;CmJMuOpBD+ql&Z-qS@D+u@TbMC}`N`s{&dvOBwJbRAE zLp+3m##X^)7;YcV1Z(C9Y|4hgxRaj7v^r-_`~kdw`OhB? zeqhRdy}V$M7hyLP`!T|c6mU9!%vAu(HCgsZgRQJwYvwAI&1QzL$3D0GARG-FaUrnN z=+C)#{yFykn{*ERb_u}_K8IW$gYAPuQ%*A5tW^ z5Wl87jtarVIj1u}Com||OFsV15`rBZV9JZ!N?V4!%&k_MBunNlWshmFyO}D0WimT0 zgSSK`Lq%m8!>y=9IOv+Uivd`4$nkBG-G5+Q|5%Lc;43&_nnv345Q#YmX)%)luxjS+ zy^~-cAXtWhMQxMeMkUa^N@?E14gibCQKo;U1^ar=LL&PTQXY3A(}dlR*JuP|KAmaG zm=-e#_Q4FWI~=T%&&1ZqWm1MkmrC>AUitaEALDV9?8gfTcJLYQh$26HFB9zJD?{$( z@YT!_*d59q(_kOclGtdQL4f-)Z=B37mF7LN|2dr?e&mOSOA2=Id8w3%!3KT?GFsrp zRP2Sid^igXgEW^w;c)DMh0r#UaF8mj(ORg#-hzO{N#R0jHY&$nzSBqovgn8#xK~K3mXgwNhZbY0|PS z3-;}W1UvXL-M+rJdCX$BPgQIh%wv`=V(HsrFE1ik1jcMMTpX+ z5G;3!L#*eN+|n6fEV0lV)~{CCSgHu@oy&s#yx=vrlVFKA<1xC~;8e`zDoZ0Xz^ViW z>!9KKXpNEY4_S%Ti-EmZ>>}xGFy>n|9Dzrp5WS6Naj@zvuqr85l`DK*uyGiKVKAu1 zwlvrU1xtff$H6!rGOO6+8|;lv2ZOWGgkuoG#=~GgLWSd+|6EA01+NGs_8&N!i`zRG z!N3a=KX+QIbAYvy4SbKv@uG%-BhlrK6@R|aP7Lg;3G4fgLeSakwj#OrgPFcMcw4D6#BU>{cKAa}~fK5m_G;VJe- z1Y0`WA7tSY~V8~hs-la@)iG0rm`}$>a-E=|wvY9Dyq)Npb;6>bE z%t8tbGWi)`cbQ@gtjf#qLvK7Dh54w^Qm(UjTKqY>g!9uvcg527RVP=9)EYxh^n%Ga z5s<*D2zK|xrGb^(@8jhX6lt|zi7oJ8(7?uFhIc%d7K~0^mP`0}$1?Jv5#q(SM&e|p zv?>$WX650Di#aQ|?p3OEWq-=T5e!Btuu7-1X!eK&qp?)N|MtcI%vr=MyvLk)gMLG74PFcq}&u%spJJd#IqllfVXoN?PM>Kd^mly`1Rb^tG>kBS7{1B zn@nM``zfWhSzsTQ5Uf<`tEFg@QpE!-k2OsR|N5EYf}Jc8j4>v$_|MeU{j=?>Vy0gz zr6nqP92f{Ds z1^WfRkXYePje{T@S4uW#gE3K1 zb;R*9bu$yc?lE5(|0y=}eI{6`1Sg20KL|&q*!rt^0E5I?!lZZ{Y~}WSOnI9OpieKf z@d)?PVTsKIuxd8DKrBuP#_zVU`+?v8W8P!p=ho> zy^lU7Sn9gz{3q0}@ayM&t_-@-@CJd0?amq>l3gFWSg!x*6tMUERr<0Ofc5!yVARDX zY#iIomW$>BH`tHeH~K#PwU+tz&tI8E+3xqbJIqQpiyt%u!$ZAlpXZL_UlO~0{}cS0 z2!>)lRYrf}4dr}4o|Ts?ra5Q&cyaQAK>8b2bKOsRZkiQ2KZO3_m= z$BD1?-G2bNyjVKcI3!fR-;kqG{POX989zD?n>ua&Cgz$ib^HgvT%9kmh8+()Z(>>F zlw)L-BJ2?!tj+#fA9S+(X0f=5>X1VDs9CVUV3J6-DM@qnvKfLM#P@5z`)RJr1g|7% zlOmD4fn!&8qa^{O`Bn5g>S8Cs?&J3YGmz0$%gF;|c#SH|jI!rM1r9TeC&|{9VdEjaukMlbD$5AAn1cO-2 z(Z5rywk!sPo66xp_6N2H*Y zYkAm7HS@=86y_&>f6N0hkCK%%?ad#-^+wZ5jvYC|MxeV#Z5~+$c6AVmr-4Dje{6TM z**+^GE^iDa*=&-{vt_5K{rX4zW8AO!D=P`oNXC!JIOPoXynZ&@u^+Fko$@ar*vanV z|1oYR2<*e7l5E?Kh;2ufw0ZK!1?{ya$*LW<=O73@hc|J)Z^v|-_}`3=;x0A=?Dm=s z^hH=3dl{8z+f1#f6hP86YVKAJ8qu3+aUR7``YnpjX9cTT6Hy$rOkTWQmZMRxSHvUX3fyk3!45QYF zHxL#*Gf)S0oE~f%JYPDcw(=;>kgSEB$XZ=e)=Ee8r5=aJ) z!wH3K4u#86g|Zb`FdR?#9PWe*Yrye%M}C}6 z9jAezWD@>h3vTVuA1lT?gq}7C!l-n3Ifi@{WXL5OQN19N3_TnsMt%}4-0)|nxL{|3 zC6eW!T*q}~#>EZN(f~3eBFQ!`U}Tq^LEaFTI#u-`7+9D&WSPxY@zcTokv=KdX<+x? zclwfKLK$kSrC>2m^cRMfBl|up9m#Bm9-#5tWpe#iuWOFNxLCZv+rWR-8Kl}+fy}`K z>pRB;JLTt_P%@_}Nf{Nvj+_*kg$cy*Lq5-Tpv_dp1+v$db`0|THE_AWg?czNpmuZ) zCzi}H@ehvq;3FeRO@|A1J{U-5OOlj#!_+j#mf;IZ(xV}qFOy@S_yxs;<#X^{Y2WW`yg3P(~7*1c<6vwa1iPn z4rDA|C4MNqT&-5Sl#ccW3d;3RF9xA95;Yo?qc+AF4xANgIp@LD&iO2`+xOS-d`qiv zsh|i}v|~V09O0)w!E$+{Itu>uXzk+R`22MZe+*Sov2fO+>cF>%iK;th6%EeUoR5zS zcIwX%f@F_qBZPt7bX+Q{5K^HZgcOBD41Wgx^l0t(3ySvU_Zt2fs=+H#RTaB6gowpF zVDjPUQOm+s#m09Yoe=DFu-o_VJyt>HjEZ0uR)G*vg@zAj5URpvl9rB&&&KO^f4@La zd-Z#lo_yzWX;flyd>@YL{R!2jMvm;XcHkoe-9>$TQn1s1>Jt*i!~lE znBp*)1eO&})I>Y;3yap35pxITvPPyuUw5bE%32;o1iWW%c3O z^giqyFvuV3CjR&-FG+P($7NL=0+$zBuuH?aDxa%DIO0QC3x(g7`N`_vU_*T7okG4t zPIO#qPB7@!mSVB-s2OogHZ^TieK13?Gk#7N$v(l8|0dMoLPFY|pUmPq0}S)WL)8{V zu>z&6wpvJ*6mJB;1*DVFp{vR+Eu;nj-!k~vh2P)IE!*=qzvJTO+<}<^_v_v5LP@?jl%E+H!huiyMKgYMNYZ(g(IIzFzwY`BKOq{7mm{82aw!$T~Q)gCEH4!{~s z5q}18b|9YfL;e_yk6c^V^$M1)SV!P81H-Zn#h~RA{F>^b$);S z`b})FU;oZ$7o-YODOg+-61?5qLlgYmIj)$t;j z>RQxgDPE{91NPE~(5(&kaNzrgtXdTt-lf(z=$S3*W>$DQ(}e6MJpe_)CgE624foK4 zHUsm5fg5uf^a1^A6(;)NRMmZaN+6yGwgQr^eS%k_L>m;_*&)ZF3Kp3L?9Z@G;oK7r zL=FvBbJFCnM)`<6nnliJQV-k6W->B+s0;43NG;YFoC0Dn3@n_6Q(7MVY!P??Y0OaZ z5mZg%33A;)2WvJVKCsVX11SS6hIF244~v0y1VNOE>)!1pANs_DaqY3u7my74 z%c^3e$S6-+_|+y01@jHqvANbE7lb+oDWgQPDM~WQdLZfIVk^Np>;z6wCOzYj_Fx<+ z3Ph}_M~`F_gue0kj1D#rSWH$Cm}VFuN4zd1gMo4gIYhy599W}ZVhqB;B=TCBf^j3c z7-Ub06k)6RKBxkD7LpPa!#8$$a1**qdI^>DxaN5j-ZU9j0_S)xRtj(Omc|VQ1Ow^( zUhmMuF9I^R&?AC@ReO^TVrg!1F0T2W%E-v@ zv8RHD4g#2x$e<`Z+D3tgdco8r7>zve(_{EtE*g)y;^2e;gJ$qCTX@j5l+foJF*Mo| zK3hU6zNDIb*)C-S$)>z@pOXo9l_!J$IgQc=7~Bo8|z z;^J|$AhE+o2uk^Z1ta)8?`R8pLo=`zIkI}l1umqxE(XSvK4{k0>vd695T$oy(I*~xT8w)saP-*dp^#=9s>suJvb=of!_lKviM|rb$sA1 zC~+8&*alzHQ#ck2LkRsA&Cg@)GUK8|e^D@g3PWTf#R60gof&KEaX(qtVICuqLf(>u z5RxcL*gJv~EJ_~b^3f3yfCi&m+=tZ zIDxD^!bgMG>qVD^V=o!RGQhOu^(f3d3dbI5VT{7if($WXM|>lT#qJ1yoNj{31-_NS zijoYxapVYQyG88bhVqDUUD9KdQ8Ge%w2F_CuW2f)5oC+;U`{#G4d-A60ih0IvqLL!CoIM$kO89jglk(7(fyK*u|;b{=f zVjmoKD)eweB~1s#vbCBu7KTaMxMZ+Ivxg9lVz=9^m&oTGOw{0R>|r_PQWTmj_o8z$ z+BMTw_)4hwIIM}QL$(3MaMj9tEv3F7|sF9e3ZG( z3CoegNBGC}igygrO7SS`SgqC(A@+K%gtg?#5eJV>=6{**ve`NSX3@CO!5SntCD)u>i-X1C_%Vo9sTT@`dd5H= z3pt>}mzjS=Rc8I^D6!OdITnnqMO3T+%fdiaGE{tpc9y(I7p#CZS~%3L@6v zJ3EmCu`*M#9kEVEbWwC3Sv#0pp#Z|_W$->*!E`AZ#@%afuBE_IqJ8{ewQOtXLM`V; zhql;7(!n-`l#WHNR~h#LWec+pk5)HBYH4K3-q9HM(U|w0VEo z!9>mRSU^TeuzY;ShMyKC!6Vd}rtK^hr`hZ4kCP}|jB8miE*ixnp%uv&p=!j*VjbKC zW63hwF(1Xboz1|dy+mPnySX}VC5A;&xTstg0ZWNSXa+tw9q)8idOXG~^wuJ$Ee1)N zz>v==m)X)IN`lxPy^2JI)S5h#FIV&p#s<2@{pkc=JZ?ox`98p{ zGO7)|QeIzukYFt?*9F12XbkP+M^Dz*)lQxJ*2(wMJFKH4=wx(2(SsgX<_RN#>h(JU z+p^wK*Vmt5CS+Jk$#qe%V`vW_udc7l**d@drFSZ7k^ZBKWqXV_!(vCDJ{7YWJB2rGj-APh@v1s%wf>lk#e;B3tV;kpj>g!^ zrL3O5c`1q}{&YV5r%kETp}TDc$4{agv-r(q z{tMrE{GxI+|H)&{L{urUE`)W7V1Ho|nbK{I`wQYdc=F`Q^bKg3@!&y>6hU#S3yO8= zV2N%Fj_B4tKF8KL6G2^uR#yTRv5{~D$LLNH#vaqfOECm literal 0 HcmV?d00001 diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml index fffcc806a..11b564b99 100644 --- a/helm/www/lambdadelta/web/home/home.ldw.xml +++ b/helm/www/lambdadelta/web/home/home.ldw.xml @@ -41,6 +41,7 @@ + diff --git a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma index 81d324bad..d62edd8ed 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/exteq.ma @@ -36,4 +36,3 @@ lemma exteq_sym (A) (B): symmetric … (exteq A B). lemma exteq_trans (A) (B): Transitive … (exteq A B). /2 width=1 by exteq_repl/ qed-. - -- 2.39.2