]> matita.cs.unibo.it Git - helm.git/blob - helm/coq-contribs/SUBSETS/README
1. change_tac moved from PrimitiveTactics to ReductionTactics
[helm.git] / helm / coq-contribs / SUBSETS / README
1
2                           Contribution  Padova/SUBSETS
3                           ============================
4
5 This directory contains a formalization in Coq of the content of this paper
6 describing a theory of subsets on a intuitionistic a predicative foundation:
7
8 G.Sambin, S.Valentini: 
9 Building up a toolbox for Martin-Lof's type theory: subset theory.
10 In Proc. of Twenty-five years of constructive type theory,
11 Oxford U.P. (1998) pp. 221-244.
12
13 Author & Date: Ferruccio Guidi
14                Department of Computer Science, University of Bologna
15                March 2005
16 E-mail : fguidi@cs.unibo.it
17 WWW    : http://www.cs.unibo.it/~fguidi
18
19 Installation procedure:
20 -----------------------
21
22   To get this contribution compiled, type
23
24     make 
25
26   or
27
28     make opt
29
30   The main modules produced by the compilation are:
31
32      Toolbox   provides the theory of subsets and its prerequisites
33
34      Base      provides just the prerequisites
35
36 Description:
37 ------------
38
39 Further information on this contribution:
40 -----------------------------------------
41
42   The latest version of this development is maintained in the CVS repository
43   of the HELM project <helm.cs.unibo.it> and can be downloaded at: 
44    
45   www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz