X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FSUBSETS%2FREADME;fp=helm%2Fcoq-contribs%2FSUBSETS%2FREADME;h=caf37357dad9f12e45edb76c8d2f6eed69c8e949;hb=65f400affe20fa3fe66b9a998ced5d6f64a23b45;hp=0000000000000000000000000000000000000000;hpb=50377dde5b5b1a8e5c7b2fb48b47defde9508b50;p=helm.git

diff --git a/helm/coq-contribs/SUBSETS/README b/helm/coq-contribs/SUBSETS/README
new file mode 100644
index 000000000..caf37357d
--- /dev/null
+++ b/helm/coq-contribs/SUBSETS/README
@@ -0,0 +1,45 @@
+
+                          Contribution  Padova/SUBSETS
+                          ============================
+
+This directory contains a formalization in Coq of the content of this paper
+describing a theory of subsets on a intuitionistic a predicative foundation:
+
+G.Sambin, S.Valentini: 
+Building up a toolbox for Martin-Lof's type theory: subset theory.
+In Proc. of Twenty-five years of constructive type theory,
+Oxford U.P. (1998) pp. 221-244.
+
+Author & Date: Ferruccio Guidi
+               Department of Computer Science, University of Bologna
+               March 2005
+E-mail : fguidi@cs.unibo.it
+WWW    : http://www.cs.unibo.it/~fguidi
+
+Installation procedure:
+-----------------------
+
+  To get this contribution compiled, type
+
+    make 
+
+  or
+
+    make opt
+
+  The main modules produced by the compilation are:
+
+     Toolbox   provides the theory of subsets and its prerequisites
+
+     Base      provides just the prerequisites
+
+Description:
+------------
+
+Further information on this contribution:
+-----------------------------------------
+
+  The latest version of this development is maintained in the CVS repository
+  of the HELM project <helm.cs.unibo.it> and can be downloaded at: 
+   
+  www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz