Dummy dependent types are no longer cleaned in inductive type arities.

[helm.git] / helm / www / matita / library.shtml

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 57f54e2bdbf62e3e63485d9ca7ef9b9f7b8aeecd..c22db5e1ce9f03802dcbcb812811ff85175bef68 100644 (file)
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -58,6 +58,11 @@
          here</a>.
       </p>
 
+      <h2>The Formal System &lambda;&delta; (lambda-delta)<a name="lambda-delta"></a></h2>
+      <p>
+      See the <a href="http://helm.cs.unibo.it/lambda-delta/">&lambda;&delta; home page</a>.
+      </p>
+
       <!--#include virtual="bottombar.shtml" -->
     </div>
   </body>