New Makefile and minor changes

Author: vladimirias

Coq_patches/README

@@ -1,4 +1,4 @@
-This directory contains patches for Coq-8.3pl2 written by Hugo Hereblin and Dan Grayson which are needed for proper compilation of the "Foundations" library. 
+This directory contains patches for Coq-8.3pl2 written by Hugo Hereblin and Dan Grayson which are needed for proper compilation of the "Foundations" library. The source code for Coq-8.3pl2 can be found at http://coq.inria.fr/distrib/  .
 
 Hugo's patches "inductive-indice-levels-matter-8.3.patch" and "patch.type-in-type" are intended only as a temporary solution for the universe management issues in Coq which arise in connection with the univalent approach. 
 

Generalities/uu0.v

@@ -17,7 +17,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (* Add LoadPath ".." as Foundations. *)
 
-Require Export Foundations.Generalities.uuu.
+Require Export "uuu".
 
 (** Universe structure *)
 
@@ -28,7 +28,6 @@ Definition UU := Type .
 
 
 
-
 (** ** Some standard constructions not using identity types (paths) *)
 
 (** *** Canonical functions from [ empty ] and to [ unit ] *)

Generalities/uuu.v

@@ -65,8 +65,6 @@ Definition pr2 { T: Type } { P : T -> Type } ( tp : total2 P ) : P ( pr1 tp ) :=
 
 
 
-
-
 (*
 
 (** The phantom type family ( following George Gonthier ) *)

Make

@@ -1,6 +1,74 @@
-# -*- makefile-gmake -*-
-include Make.makefile
-COQDEFS := --language=none -r '/^[[:space:]]*\(Axiom\|Theorem\|Class\|Instance\|Let\|Ltac\|Definition\|Lemma\|Record\|Remark\|Structure\|Fixpoint\|Fact\|Corollary\|Let\|Inductive\|Coinductive\|Proposition\)[[:space:]]+\([[:alnum:]_]+\)/\2/'
-TAGS : $(VFILES); etags $(COQDEFS) $^
-clean:clean2
-clean2:; rm -f TAGS
+all : hlevel2/hq.vo hlevel2/finitesets.vo  Proof_of_Extensionality/funextfun.vo
+
+hlevel2/hq.vo : hlevel2/hq.v hlevel2/hz.vo
+	cd hlevel2/ && coqc hq
+hlevel2/hz.vo : hlevel2/hz.v hlevel2/hnat.vo
+	cd hlevel2/ && coqc hz
+
+hlevel2/finitesets.vo : hlevel2/finitesets.v hlevel2/stnfsets.vo
+	cd hlevel2/ && coqc finitesets
+hlevel2/stnfsets.vo : hlevel2/stnfsets.v hlevel2/hnat.vo
+	cd hlevel2/ && coqc stnfsets
+
+hlevel2/hnat.vo : hlevel2/hnat.v hlevel2/algebra1d.vo
+	cd hlevel2/ && coqc hnat
+hlevel2/algebra1d.vo : hlevel2/algebra1d.v hlevel2/algebra1c.vo
+	cd hlevel2/ && coqc algebra1d
+hlevel2/algebra1c.vo : hlevel2/algebra1c.v hlevel2/algebra1b.vo
+	cd hlevel2/ && coqc algebra1c
+hlevel2/algebra1b.vo : hlevel2/algebra1b.v hlevel2/algebra1a.vo
+	cd hlevel2/ && coqc algebra1b
+hlevel2/algebra1a.vo : hlevel2/algebra1a.v hlevel2/hSet.vo
+	cd hlevel2/ && coqc algebra1a
+
+hlevel2/hSet.vo : hlevel2/hSet.v hlevel1/hProp.vo
+	cd hlevel2/ && coqc hSet
+
+hlevel1/hProp.vo : hlevel1/hProp.v Generalities/uu0.vo
+	cd hlevel1/ && coqc hProp
+
+Proof_of_Extensionality/funextfun.vo : Proof_of_Extensionality/funextfun.v Generalities/uu0.vo
+	cd Proof_of_Extensionality/ && coqc funextfun
+
+Generalities/uu0.vo : Generalities/uu0.v Generalities/uuu.vo
+	cd Generalities/ && coqc uu0
+Generalities/uuu.vo : Generalities/uuu.v
+	cd Generalities/ && coqc uuu
+
+
+clean : 
+	rm -f Generalities/*.vo Proof_of_Extensionality/*.vo hlevel1/*.vo hlevel2/*.vo
+	rm -f Generalities/*.glob Proof_of_Extensionality/*.glob hlevel1/*.glob hlevel2/*.glob
+
+
+
+#
+# The following is copied from a makefile generated by coq_makefile V8.3pl5
+#
+
+
+VFILES:=Generalities/uuu.v\
+  Generalities/uu0.v\
+  Proof_of_Extensionality/funextfun.v\
+  hlevel1/hProp.v\
+  hlevel2/hSet.v\
+  hlevel2/algebra1a.v\
+  hlevel2/algebra1b.v\
+  hlevel2/algebra1c.v\
+  hlevel2/algebra1d.v\
+  hlevel2/hnat.v\
+  hlevel2/stnfsets.v\
+  hlevel2/finitesets.v\
+  hlevel2/hz.v\
+  hlevel2/hq.v
+VOFILES:=$(VFILES:.v=.vo)
+
+COQLIB:=$(shell $(COQBIN)coqtop -where | sed -e 's/\\/\\\\/g')
+
+install : 
+	mkdir -p $(COQLIB)/user-contrib
+	(for i in $(VOFILES); do \
+	 install -d `dirname $(COQLIB)/user-contrib/Foundations/$$i`; \
+	 install $$i $(COQLIB)/user-contrib/Foundations/$$i; \
+	 done)
+

Make.makefile

@@ -11,9 +11,9 @@ This file contains the formulation of the univalence axiom and the proof that it
 
 Unset Automatic Introduction. (** This line has to be removed for the file to compile with Coq8.2 *)
 
-(* Add LoadPath ".." as Foundations. *)
+Add LoadPath "../Generalities".
 
-Require Export Foundations.Generalities.uu0.
+Require Export "uu0".
 
 
 (** ** Univalence axiom. *)

Makefile

@@ -1,4 +1,4 @@
-By Vladimir  Voevodsky Feb. 2010 - Nov. 2013 .
+By Vladimir  Voevodsky Feb. 2010 - Dec. 2013 .
 
 This is the current version of the mathematical library for the proof assistant Coq based on the univalent semantics for the calculus of inductive constructions. The best way to see in detail what the files in these subdirectories are about is to generate the corresponding tables of content with coqdoc . Here we give a brief outline of the library structure .   
 
@@ -28,4 +28,6 @@ At the end of files finitesets.v,  hz.v and hq.v there are sample computations w
 
 Directory Proof_of_Extensionality/ contains the formulation of general Univalence Axiom and a proof that it implies functional extensionality . 
 
+The easiest way to compile the library is by typing "make" in this directory. For this to work one should have GNU Make installed which is easly to find on the web. 
 
+Once the library is compiled the individual files of the library can be followed line-by-line in CoqIDE or Proof General. 

Proof_of_Extensionality/funextfun.v

@@ -25,9 +25,9 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
 
 (** Imports *)
 
-(* Add LoadPath ".." as Foundations. *)
+Add LoadPath "../Generalities" .
 
-Require Export Foundations.Generalities.uu0 . 
+Require Export "uu0" . 
 
 (** Universe structure *)