Skip to content

Commit

Permalink
Changed Makefile such that RezkCompletion compiles as before.
Browse files Browse the repository at this point in the history
  • Loading branch information
@vladimirias
vladimirias committed Jan 3, 2014
1 parent 4f932c4 commit 6c7aa56
Show file tree
Hide file tree
Showing 13 changed files with 88 additions and 24 deletions.
28 changes: 14 additions & 14 deletions Makefile
View file
@@ -1,39 +1,39 @@
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
cd hlevel2/ && coqc -R . Foundations.hlevel2 hq
hlevel2/hz.vo : hlevel2/hz.v hlevel2/hnat.vo
cd hlevel2/ && coqc hz
cd hlevel2/ && coqc -R . Foundations.hlevel2 hz

hlevel2/finitesets.vo : hlevel2/finitesets.v hlevel2/stnfsets.vo
cd hlevel2/ && coqc finitesets
cd hlevel2/ && coqc -R . Foundations.hlevel2 finitesets
hlevel2/stnfsets.vo : hlevel2/stnfsets.v hlevel2/hnat.vo
cd hlevel2/ && coqc stnfsets
cd hlevel2/ && coqc -R . Foundations.hlevel2 stnfsets

hlevel2/hnat.vo : hlevel2/hnat.v hlevel2/algebra1d.vo
cd hlevel2/ && coqc hnat
cd hlevel2/ && coqc -R . Foundations.hlevel2 hnat
hlevel2/algebra1d.vo : hlevel2/algebra1d.v hlevel2/algebra1c.vo
cd hlevel2/ && coqc algebra1d
cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1d
hlevel2/algebra1c.vo : hlevel2/algebra1c.v hlevel2/algebra1b.vo
cd hlevel2/ && coqc algebra1c
cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1c
hlevel2/algebra1b.vo : hlevel2/algebra1b.v hlevel2/algebra1a.vo
cd hlevel2/ && coqc algebra1b
cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1b
hlevel2/algebra1a.vo : hlevel2/algebra1a.v hlevel2/hSet.vo
cd hlevel2/ && coqc algebra1a
cd hlevel2/ && coqc -R . Foundations.hlevel2 algebra1a

hlevel2/hSet.vo : hlevel2/hSet.v hlevel1/hProp.vo
cd hlevel2/ && coqc hSet
cd hlevel2/ && coqc -R . Foundations.hlevel2 hSet

hlevel1/hProp.vo : hlevel1/hProp.v Generalities/uu0.vo
cd hlevel1/ && coqc hProp
cd hlevel1/ && coqc -R . Foundations.hlevel1 hProp

Proof_of_Extensionality/funextfun.vo : Proof_of_Extensionality/funextfun.v Generalities/uu0.vo
cd Proof_of_Extensionality/ && coqc funextfun
cd Proof_of_Extensionality/ && coqc -R . Foundations.Proof_of_Extensionality funextfun

Generalities/uu0.vo : Generalities/uu0.v Generalities/uuu.vo
cd Generalities/ && coqc uu0
cd Generalities/ && coqc -R . Foundations.Generalities uu0
Generalities/uuu.vo : Generalities/uuu.v
cd Generalities/ && coqc uuu
cd Generalities/ && coqc -R . Foundations.Generalities uuu


clean :
Expand Down
1 change: 1 addition & 0 deletions Proof_of_Extensionality/funextfun.v
View file
Expand Up @@ -13,6 +13,7 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co

Add LoadPath "../Generalities".

Require Export "uuu".
Require Export "uu0".


Expand Down
1 change: 1 addition & 0 deletions hlevel1/hProp.v
View file
Expand Up @@ -27,6 +27,7 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com

Add LoadPath "../Generalities" .

Require Export "uuu".
Require Export "uu0" .

(** Universe structure *)
Expand Down
5 changes: 4 additions & 1 deletion hlevel2/algebra1a.v
View file
Expand Up @@ -16,7 +16,10 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export hSet .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .


(** To upstream files *)
Expand Down
6 changes: 5 additions & 1 deletion hlevel2/algebra1b.v
View file
Expand Up @@ -16,7 +16,11 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export algebra1a .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .


(** To upstream files *)
Expand Down
7 changes: 6 additions & 1 deletion hlevel2/algebra1c.v
View file
Expand Up @@ -16,7 +16,12 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export algebra1b .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .


(** To upstream files *)
Expand Down
8 changes: 7 additions & 1 deletion hlevel2/algebra1d.v
View file
Expand Up @@ -16,7 +16,13 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export algebra1c .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .


(** To upstream files *)
Expand Down
11 changes: 10 additions & 1 deletion hlevel2/finitesets.v
View file
Expand Up @@ -21,7 +21,16 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export stnfsets .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .
Require Export "algebra1d" .
Require Export "hnat" .
Require Export "stnfsets" .



Expand Down
5 changes: 4 additions & 1 deletion hlevel2/hSet.v
View file
Expand Up @@ -20,7 +20,10 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export hProp .

Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .



Expand Down
9 changes: 8 additions & 1 deletion hlevel2/hnat.v
View file
Expand Up @@ -20,7 +20,14 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export algebra1d .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .
Require Export "algebra1d" .

(** To up-stream files *)

Expand Down
11 changes: 10 additions & 1 deletion hlevel2/hq.v
View file
Expand Up @@ -19,7 +19,16 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export hz .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .
Require Export "algebra1d" .
Require Export "hnat" .
Require Export "hz" .

Opaque hz .

Expand Down
10 changes: 9 additions & 1 deletion hlevel2/hz.v
View file
Expand Up @@ -19,7 +19,15 @@ Unset Automatic Introduction. (** This line has to be removed for the file to co
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export hnat .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .
Require Export "algebra1d" .
Require Export "hnat" .



Expand Down
10 changes: 9 additions & 1 deletion hlevel2/stnfsets.v
View file
Expand Up @@ -18,7 +18,15 @@ Unset Automatic Introduction. (* This line has to be removed for the file to com
Add LoadPath "../hlevel1" .
Add LoadPath "../Generalities".

Require Export hnat .
Require Export "uuu".
Require Export "uu0" .
Require Export "hProp" .
Require Export "hSet" .
Require Export "algebra1a" .
Require Export "algebra1b" .
Require Export "algebra1c" .
Require Export "algebra1d" .
Require Export "hnat" .


(* To up-stream files *)
Expand Down

0 comments on commit 6c7aa56

Please sign in to comment.