From 337862338098a2e01a8d59dab6e36663d9679067 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 8 Dec 2011 21:34:37 +0000
Subject: [PATCH] Maietti suggested to replace a paragraph about the
 development on the Basic Picture

---
 helm/www/matita/library.shtml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/helm/www/matita/library.shtml b/helm/www/matita/library.shtml
index 9874142c9..626cdaba1 100644
--- a/helm/www/matita/library.shtml
+++ b/helm/www/matita/library.shtml
@@ -71,8 +71,9 @@
            adjunction between topological spaces and locales</li>
       </ul>
       <p>
-      All the results are presented constructively and in the predicative
-      fragment of Matita, without any reference to choice axioms.
+      All the results are presented constructively and in the predicative 
+      fragment of Matita based on the minimalist type theory
+      by Maietti and Sambin, where choice axioms are not valid.
       </p>
       In order to reason conformtably on the previous concrete categories and
       functors, we also present algebraic versions of all the introduced
-- 
2.39.2