X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fweb%2Fbasic_2_src.tbl;h=850588ce1fe30ac73e1e3b6045b351d98272ea60;hb=0e16720654c6667b94433e91dddc3c53b904e200;hp=f02240094297af8b7e0cad9da7e600412b8f805b;hpb=084ea7868f6153effc18e8ee1c0e6cdb34d181c0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index f02240094..850588ce1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -20,7 +20,7 @@ table {
    class "magenta"
    [ { "dynamic typing" * } {
         [ { "context-sensitive native type assignment" * } {
-             [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_ind" * ]
+             [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" * ]
           }
         ]
         [ { "context-sensitive native validity" * } {
@@ -40,6 +40,12 @@ table {
    ]
    class "blue"
    [ { "rt-conversion" * } {
+        [ { "context-sensitive parallel eta-conversion" * } {
+             [ [ "for lenvs on all entries" ] "lpce ( ⦃?,?⦄ ⊢ ⬌η[?] ? )" * ]
+             [ [ "for binders" ] "cpce_ext" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
+             [ [ "for terms" ] "cpce" + "( ⦃?,?⦄ ⊢ ? ⬌η[?] ? )" * ]
+          }
+        ]
         [ { "context-sensitive parallel r-conversion" * } {
              [ [ "for terms" ] "cpc" + "( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ]
           }